Re: [isabelle] strange locale behaviours in presence of local definitions
locale L =
fixes c0 :: "'a => 'a"
definition "c1 x = c0 (c0 x)"
(* Doesn't work *)
(* locale M2 = L + assumes "c1 x = 3" *)
The current implementation is incomplete. The syntax introduced by
the definition is not available while M2 is read. You need to use
the global constant, applied to the parameters, instead. That is:
locale M2 = L + assumes "L.c1 c0 x = 3"
The tutorial on locale interpretation (http://cl-
elaborates on this issue.
This archive was generated by a fusion of
Pipermail (Mailman edition) and