[isabelle] "defines" in a locale
Is this supposed to work? Iâm guessing not. The error that arises is not very good (for recent repository versions and 2016-RC2).
In my actual use-case I assume âQ bâ where Q implies P, and the definition is non-trivial. As a syntactic nicety I donât want to have to provide âaâ when I instantiate locale m. I can make this work for now by saying: assumes âa = bâ but it is ugly.
locale l =
assumes "P a"
locale m = l +
(* assumes âP bâ *)
defines "a == b"
This archive was generated by a fusion of
Pipermail (Mailman edition) and