25 lines
445 B
Plaintext
25 lines
445 B
Plaintext
|
false = t
|
||
|
|
true = t t
|
||
|
|
|
||
|
|
triage = (\a b c : t (t a b) c)
|
||
|
|
|
||
|
|
matchBool = (\ot of : triage
|
||
|
|
of
|
||
|
|
(\_ : ot)
|
||
|
|
(\_ _ : ot)
|
||
|
|
)
|
||
|
|
|
||
|
|
not_TC? = t (t (t t) (t t t)) (t t (t t t))
|
||
|
|
not_Lambda? = matchBool false true
|
||
|
|
|
||
|
|
areEqual? = equal not_TC not_Lambda
|
||
|
|
|
||
|
|
true_TC? = not_TC false
|
||
|
|
false_TC? = not_TC true
|
||
|
|
|
||
|
|
true_Lambda? = not_Lambda false
|
||
|
|
false_Lambda? = not_Lambda true
|
||
|
|
|
||
|
|
areTrueEqual? = equal true_TC true_Lambda
|
||
|
|
areFalseEqual? = equal false_TC false_Lambda
|