[Why3-club] Specializing theories containing axioms

Jean-Christophe Filliâtre Jean-Christophe.Filliatre at lri.fr
Thu Apr 7 13:41:36 CEST 2011


> PS: By the way, the formal grammar states that axiom/lemma/goal have to
> be followed by uident/uqualid, while Why3 is perfectly fine with
> lower-cased identifiers. And I'm too, as a user.

the documentation is fixed (in git, not online)

-- 
Jean-Christophe



More information about the Why3-club mailing list