Hi Florian,
to me the liberal flag seems rather ad-hoc. Wouldn't a proper
hierarchical naming solve this problem (maybe by introducing an
automatic "sub-module" Internal/Auto/Whatever for any theory T, such
that automatic names may be referred to by using T.Whatever.automatic_name).
Admitted
Typically, bindings are created by the user in the theory text and
passed down from there, e.g.
specification (definition) foo :: T
where
"P foo"
creates a @{binding foo}.
However in packages often also bindings are created automatically.
Currently I am working on some fragements of a me
On 10/07/2010 09:11 AM, Florian Haftmann wrote:
I'm currently working on a package for generic type mappers. Leaving
aside matters like contravariance and such, a type mapper
map_k :: ('a_1 => 'b_1) => ... => ('a_n => 'b_n)
=> ('a_1, ..., 'a_n) k is => ('b_1, ..., 'b_n) k
for an
I'm currently working on a package for generic type mappers. Leaving
aside matters like contravariance and such, a type mapper
map_k :: ('a_1 => 'b_1) => ... => ('a_n => 'b_n)
=> ('a_1, ..., 'a_n) k is => ('b_1, ..., 'b_n) k
for an n-ary type ('a_1, ..., 'a_n) k must satisfy some character
