2
module NamedImplicit where
6
map' : (A B : Set) -> (A -> B) -> T A -> T B
8
map : {A B : Set} -> (A -> B) -> T A -> T B
19
id : {A : Set} -> A -> A
22
const : {A B : Set} -> A -> B -> A
26
unsafeCoerce : {A B : Set} -> A -> B
28
test1 = map {B = Nat} id
29
test2 = map {A = Nat} (const zero)
30
test3 = map {B = Bool} (unsafeCoerce {A = Nat})
31
test4 = map {B = Nat -> Nat} (const {B = Bool} id)
34
f : {A B C D : Set} -> D -> D
35
f {D = X} = \(x : X) -> x