25 lines
863 B
Plaintext
25 lines
863 B
Plaintext
|
false = t
|
||
|
|
true = t t
|
||
|
|
_ = t
|
||
|
|
k = t t
|
||
|
|
i = t (t k) t
|
||
|
|
s = t (t (k t)) t
|
||
|
|
m = s i i
|
||
|
|
b = s (k s) k
|
||
|
|
c = s (s (k s) (s (k k) s)) (k k)
|
||
|
|
iC = (\a b c : s a (k c) b)
|
||
|
|
yi = (\i : b m (c b (i m)))
|
||
|
|
y = yi iC
|
||
|
|
triage = (\a b c : t (t a b) c)
|
||
|
|
pair = t
|
||
|
|
matchList = (\oe oc : triage oe _ oc)
|
||
|
|
lconcat = y (\self : matchList (\k : k) (\h r k : pair h (self r k)))
|
||
|
|
hmap = y (\self : matchList (\f : t) (\hd tl f : pair (f hd) (self tl f)))
|
||
|
|
map = (\f l : hmap l f)
|
||
|
|
lAnd = triage (\x : false) (\_ x : x) (\_ _ x : x)
|
||
|
|
lOr = triage (\x : x) (\_ _ : true) (\_ _ x : true)
|
||
|
|
equal = y (\self : triage (triage true (\z : false) (\y z : false)) (\ax : triage false (self ax) (\y z : false)) (\ax ay : triage false (\z : false) (\bx by : lAnd (self ax bx) (self ay by))))
|
||
|
|
|
||
|
|
x = map (\i : lconcat "Successfully concatenated " i) [("two strings!")]
|
||
|
|
equal x [("Successfully concatenated two strings!")]
|