Re: [isabelle] Question about functions with equal names defined in different theories

On Wed, 22 Sep 2010, Andreas Lochbihler wrote:

theory Foo imports Main begin
definition foldl :: "nat" where "foldl = 0"

notation List.foldl ("foldl")
term "foldl" -- "List.foldl"

no_notation List.fold ("foldl")
term "foldl" -- "Foo.foldl"

For tricks like this I recommend using 'abbreviation' instead, since it does not spoil the token table of the syntax with literal "foldl" etc.

More hardcore manipulations can be done with name space aliases in Isabelle2009-2, e.g. like this:

  setup {* Sign.const_alias @{binding fold} @{const_name List.foldr} *}
  hide_const List.foldr

  term fold
  term foldr  -- "free variable"

Workarounds with aliases are not much worse than 'hide_const' etc. Of course, we are all waiting for proper name space management at the level of theory "modules", "packages", whatever. After a few more rounds of "localization" of old packages we are getting closer and closer to that.


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