[Why3-club] "if formula then" in expressions?

Guillaume Melquiond guillaume.melquiond at inria.fr
Wed Nov 7 09:48:55 CET 2012


Le mercredi 07 novembre 2012 à 09:30 +0100, Alan Schmitt a écrit :
> > This is not a bug. Possibly, the thing you are missing is that "x < y"
> > is a formula. (Sure, decidable formulas are just a tiny part of all the
> > formulas, so I understand how troubling such if-then-else expressions
> > might be.)
> 
> Well, according to Figures 7.3 and 7.7 of the manual, it's both a
> formula and an expression (since '<' is an "infix-op"). What I have
> trouble understanding is the mismatch between Figure 7.7 (where an "if"
> can only take an expression as conditional argument) and the
> implementation.

Figure 7.3 applies to theories while Figure 7.7 applies to modules.
There are a lot of redundancies between both entities (and ultimately
they should be completely redundant, so as to avoid surprises, in my
opinion), but they are still separated.

> Related questions are: what is the type of the expression (not formula)
> "x = y"? And what is the expected type of "expr" in the expression "if
> expr then ..."?

They have the type of formulas in first-order logic (or Prop for Coq).
In particular, expr is not a boolean: "if some_bool then" is ill-typed.

Best regards,

Guillaume




More information about the Why3-club mailing list