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



Hi Michael,

locale L =
  fixes c0 :: "'a => 'a"
begin
  definition "c1 x = c0 (c0 x)"
end

(* 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- informatik.uibk.ac.at/users/clemens/publications/TUM-I0723.pdf) elaborates on this issue.

Clemens





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