mirror of
https://github.com/HigherOrderCO/Kind.git
synced 2024-09-11 19:47:15 +03:00
60 lines
2.7 KiB
Plaintext
60 lines
2.7 KiB
Plaintext
// Bool : * = ∀(P: *) ∀(s: P) ∀(z: P) P
|
|
_BOOL = Kind.set
|
|
_Bool = (Kind.all "P" Kind.set λP(Kind.all "t" P λt(Kind.all "f" P λf(P))))
|
|
|
|
// True : Bool = λP λt λf t
|
|
_TRUE = _Bool
|
|
_True = (Kind.lam "P" λP(Kind.lam "t" λt(Kind.lam "f" λf(t))))
|
|
|
|
// False : Bool = λP λt λf f
|
|
_FALSE = _Bool
|
|
_False = (Kind.lam "P" λP(Kind.lam "t" λt(Kind.lam "f" λf(f))))
|
|
|
|
// AND : ∀(x: Bool) ∀(y: Bool) Bool = λx λy (x Bool y False)
|
|
_AND = (Kind.all "x" _Bool λx(Kind.all "y" _Bool λy(_Bool)))
|
|
_and = (Kind.lam "x" λx(Kind.lam "y" λy(Kind.app (Kind.app (Kind.app x _Bool) y) _False)))
|
|
|
|
// Nat : * = ∀(P: *) ∀(s: ∀(x: P) P) ∀(z: P) P
|
|
_NAT = Kind.set
|
|
_Nat = (Kind.all "P" Kind.set λP(Kind.all "s" (Kind.all "x" P λx(P)) λs(Kind.all "z" P λz(P))))
|
|
|
|
// exp : ∀(n: Nat) Nat = λn λm λP λs λz (m ∀(x:P)P (n P))
|
|
_EXP = (Kind.all "n" _Nat λn(Kind.all "m" _Nat λm(_Nat)))
|
|
_exp = (Kind.lam "n" λn(Kind.lam "m" λm(Kind.lam "P" λP(Kind.app (Kind.app m (Kind.all "x" P λx(P))) (Kind.app n P)))))
|
|
|
|
// C2 : Nat = λs λz (s (s z))
|
|
_C2 = _Nat
|
|
_c2 = (Kind.lam "P" λP(Kind.lam "s" λs(Kind.lam "z" λz(Kind.app s (Kind.app s z)))))
|
|
|
|
// C4 : Nat = λs λz (s (s (s (s z))))
|
|
_C4 = _Nat
|
|
_c4 = (Kind.lam "P" λP(Kind.lam "s" λs(Kind.lam "z" λz(Kind.app s (Kind.app s (Kind.app s (Kind.app s z)))))))
|
|
|
|
// Equal : ∀(A: *) ∀(a: A) ∀(b: A) * = λA λa λb ∀(P: ∀(x: A) *) ∀(p: (P a)) (P b)
|
|
_EQUAL = (Kind.all "P" Kind.set λA(Kind.all "a" A λa(Kind.all "b" A λb(Kind.set))))
|
|
_Equal = (Kind.lam "A" λA(Kind.lam "a" λa(Kind.lam "b" λb(Kind.all "P" (Kind.all "x" A λx(Kind.set)) λP(Kind.all "p" (Kind.app P a) λp(Kind.app P b))))))
|
|
|
|
// refl : ∀(A: *) ∀(a: A) (Equal A a a) = λA λa λP λp p
|
|
_REFL = (Kind.all "A" Kind.set λA(Kind.all "a" A λa(Kind.app (Kind.app (Kind.app _Equal A) a) a)))
|
|
_refl = (Kind.lam "A" λA(Kind.lam "a" λa(Kind.lam "P" λP(Kind.lam "p" λp p))))
|
|
|
|
// WORK : ∀(n: Nat) Bool = λn (n ∀(x:Bool)Bool λpλb(Bool.and (p b) (p b)) λx(x) True)
|
|
_WORK = (Kind.all "n" _Nat λn(_Bool))
|
|
_work = (Kind.lam "n" λn(Kind.app (Kind.app (Kind.app (Kind.app n (Kind.all "x" _Bool λx(_Bool)))
|
|
(Kind.lam "p" λp(Kind.lam "b" λb(Kind.app (Kind.app (Kind.ann _and _AND) (Kind.app p b)) (Kind.app p b)))))
|
|
(Kind.lam "x" λx(x)))
|
|
_True))
|
|
|
|
// RESULT : Bool = (work c3)
|
|
_RESULT = _Bool
|
|
_result = (Kind.app (Kind.ann _work _WORK) (Kind.app (Kind.app _exp _c2) _c4))
|
|
|
|
// MAIN : (Equal Bool result True) = λP λrefl refl
|
|
_MAIN = (Kind.app (Kind.app (Kind.app _Equal _Bool) _result) _True)
|
|
_main = (Kind.lam "P" λP(Kind.lam "refl" λrefl(refl)))
|
|
|
|
// Checks if `(work 2^4)` is propositionally equal to `true`
|
|
_OBLITERATE
|
|
: String
|
|
= (~(Kind.check _main _MAIN Nat.zero) λx(String) λt("check") "error")
|