From 0e97867813954b02bd0fcff4610978e1b27a93f5 Mon Sep 17 00:00:00 2001
From: Derenash <eyer.derenash@gmail.com>
Date: Wed, 21 Feb 2024 12:10:56 -0300
Subject: [PATCH] add Cmp files for String and U60

---
 book/String.cmp.kind2 | 22 ++++++++++++++++++++++
 book/U60.cmp.kind2    |  7 +++++++
 2 files changed, 29 insertions(+)
 create mode 100644 book/String.cmp.kind2
 create mode 100644 book/U60.cmp.kind2

diff --git a/book/String.cmp.kind2 b/book/String.cmp.kind2
new file mode 100644
index 00000000..1f33e9d3
--- /dev/null
+++ b/book/String.cmp.kind2
@@ -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)
\ No newline at end of file
diff --git a/book/U60.cmp.kind2 b/book/U60.cmp.kind2
new file mode 100644
index 00000000..530f233f
--- /dev/null
+++ b/book/U60.cmp.kind2
@@ -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)
+ 
\ No newline at end of file