Apparently, QCheck2.(false && true ==> true) is false, whereas in propositional calculus, it is standard that conjunction have precedence over implication. This is a bit puzzling and should be at least documented in the documentation of ==> and ideally fixed.
The manual https://ocaml.org/manual/5.4/expr.html#ss:precedence-and-associativity says that indeed an infix operator =... is more tight than &..., which is consistent with the above observation but tends to imply that there is no easy fix without changing the symbol ==>.
Note: the documentation https://ocaml.org/docs/operators#operator-associativity-and-precedence looks incorrect since it puts both operators in the same precedence group, which is furthermore said to be left-associative: this contradicts the above observation.
Apparently,
QCheck2.(false && true ==> true)isfalse, whereas in propositional calculus, it is standard that conjunction have precedence over implication. This is a bit puzzling and should be at least documented in the documentation of==>and ideally fixed.The manual https://ocaml.org/manual/5.4/expr.html#ss:precedence-and-associativity says that indeed an infix operator
=...is more tight than&..., which is consistent with the above observation but tends to imply that there is no easy fix without changing the symbol==>.Note: the documentation https://ocaml.org/docs/operators#operator-associativity-and-precedence looks incorrect since it puts both operators in the same precedence group, which is furthermore said to be left-associative: this contradicts the above observation.