[isabelle] "defines" in a locale



Hi,

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.

cheers,
peter

theory l
imports Main
begin

locale l =
  fixes a
  assumes "P a"

locale m = l +
  fixes b
  (* assumes âP bâ *)
  defines "a == b"

end

-- 
http://peteg.org/





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.