new material

1 files changed, 21 insertions, 1 deletions

diff --git a/hott/More_List.thy b/hott/More_List.thy
index 2f868b8..aa57635 100644
--- a/hott/More_List.thy
+++ b/hott/More_List.thy
@@ -1,8 +1,28 @@
 theory More_List
-imports Spartan.List
+imports
+  Spartan.List
+  Nat
 
 begin
 
+experiment begin
+  Lemma "map (\<lambda>n: Nat. suc n) [0, suc (suc 0), suc 0] \<equiv> ?xs"
+    unfolding map_def by (subst comps)+
+end
+
+section \<open>Length\<close>
+
+definition [implicit]:
+  "len \<equiv> ListRec ? Nat 0 (\<lambda>_ _ n. suc n)"
+
+experiment begin
+  Lemma "len [] \<equiv> 0" by reduce
+  Lemma "len [0, suc 0, suc (suc 0)] \<equiv> ?n" by (subst comps)+
+end
+
+section \<open>Equality on lists\<close>
+
+(*Hmmm.*)
 
 
 end