From b0ba102b783418560f9b7b15239681b11ea4c877 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Tue, 26 May 2020 16:50:35 +0200
Subject: new material

---
 hott/More_List.thy | 22 +++++++++++++++++++++-
 1 file changed, 21 insertions(+), 1 deletion(-)

(limited to 'hott/More_List.thy')

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
-- 
cgit v1.2.3