1
module UntypedLambda where
12
open module ULam = Syntacticosmos TT TT (\_ -> Tag)
18
SigLAM = Pi _ conk where
20
conk lamT = (LAM |> LAM) |> LAM
21
conk appT = LAM |> LAM |> LAM
24
Lam G = G [! SigLAM !]- LAM
26
lam : {G : Cxt}(x : Nom){Gx : [| G Hasn't x |]} ->
27
Lam ((G [ x - LAM ]) {Gx}) -> Lam G
28
lam x {Gx} b = G[ lamT G^ G\\ (bind x {Gx} b) G& Gnil ]
30
app : {G : Cxt} -> Lam G -> Lam G -> Lam G
31
app f s = G[ appT G^ f G& s G& Gnil ]
34
moo = lam Ze (lam (Su Ze) (var Ze))
37
noo = lam (Su Ze) (lam Ze (var (Su Ze)))