9 lines
477 B
Text
9 lines
477 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 (name arg body) ((lambda name body) arg) (let name arg body))
|
||
|
|
(def id-type (Pi a U (Pi x a a)))
|
||
|
|
(def id (lambda _ (lambda x x)))
|
||
|
|
(forall (in out) (-> in out) (Pi _ in out))
|
||
|
|
(forall (expr expected got) (assert-type expected (the got expr)) (= expected got))
|
||
|
|
(forall (a) (= a a) t)
|
||
|
|
(forall (name-a name-b in out) (= (Pi name-a in out) (Pi name-b in out)) t)
|