12 lines
617 B
Text
12 lines
617 B
Text
|
(forall (name arg type out f) ((the (Pi name type out) f) (the type arg)) (let name arg (the out (f arg))))
|
||
|
|
(forall (in out) (-> in out) (Pi _ in out))
|
||
|
|
(forall (var body arg) ((lambda var body) arg) (let var arg body))
|
||
|
|
|
||
|
|
(def succ (the (-> nat nat) +1))
|
||
|
|
(def cons (the (Pi A U (Pi B U (-> A (-> B (Pair A B))))) (lambda _ (lambda _ (lambda a (lambda b (pair a b)))))))
|
||
|
|
(def car (the (Pi A U (Pi B U (-> (Pair A B) A))) (lambda _ (lambda _ (lambda p (car' p))))))
|
||
|
|
(forall (a b) (car' (pair a b)) a)
|
||
|
|
|
||
|
|
(def our-car ((car (the U nat)) (the U symbol)))
|
||
|
|
(((((cons (the U nat)) (the U symbol)) (the nat 0)) (the symbol hi)))
|