proved a few oopses + minor tweaks

1 files changed, 1 insertions, 11 deletions

diff --git a/hott/More_List.thy b/hott/More_List.thy
index c3d63f6..a216987 100644
--- a/hott/More_List.thy
+++ b/hott/More_List.thy
@@ -5,24 +5,14 @@ imports
 
 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)"
+definition [implicit]: "len \<equiv> ListRec ? Nat 0 (\<lambda>_ _ rec. suc rec)"
 
 experiment begin
   Lemma "len [] \<equiv> ?n" by (subst comps)+
   Lemma "len [0, suc 0, suc (suc 0)] \<equiv> ?n" by (subst comps)+
 end
 
-section \<open>Equality on lists\<close>
-
-(*Hmmm.*)
-
 
 end