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 characteristic
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 n-ary
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
