Re: [isabelle] strange locale behaviours in presence of local definitions

Hi Michael,

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 MHonArc.