mirror of
https://github.com/HigherOrderCO/Kind.git
synced 2024-08-16 11:10:34 +03:00
add Cmp files for String and U60
This commit is contained in:
parent
7124036c94
commit
0e97867813
22
book/String.cmp.kind2
Normal file
22
book/String.cmp.kind2
Normal file
@ -0,0 +1,22 @@
|
|||||||
|
String.cmp
|
||||||
|
: ∀(a: String)
|
||||||
|
∀(b: String)
|
||||||
|
Cmp
|
||||||
|
= λa λb
|
||||||
|
let P = λx ∀(b: String) (Cmp)
|
||||||
|
let cons = λa.head λa.tail λb
|
||||||
|
let P = λx ∀(a.head: Char) ∀(a.tail: String) (Cmp)
|
||||||
|
let cons = λb.head λb.tail λa.head λa.tail
|
||||||
|
let P = λx Cmp
|
||||||
|
let ltn = Cmp.ltn
|
||||||
|
let eql = (String.cmp a.tail b.tail)
|
||||||
|
let gtn = Cmp.gtn
|
||||||
|
(~(U60.cmp a.head b.head) P ltn eql gtn)
|
||||||
|
let nil = λa.head λa.tail Cmp.gtn
|
||||||
|
((~b P cons nil) a.head a.tail)
|
||||||
|
let nil = λb
|
||||||
|
let P = λx Cmp
|
||||||
|
let cons = λb.head λb.tail Cmp.ltn
|
||||||
|
let nil = Cmp.eql
|
||||||
|
(~b P cons nil)
|
||||||
|
(~a P cons nil b)
|
7
book/U60.cmp.kind2
Normal file
7
book/U60.cmp.kind2
Normal file
@ -0,0 +1,7 @@
|
|||||||
|
U60.cmp
|
||||||
|
: ∀(a: #U60)
|
||||||
|
∀(b: #U60)
|
||||||
|
(Cmp)
|
||||||
|
= λa λb
|
||||||
|
(U60.if #(== a b) Cmp (U60.if #(< a b) Cmp Cmp.gtn Cmp.ltn) Cmp.eql)
|
||||||
|
|
Loading…
Reference in New Issue
Block a user