From 9ed05b8027122d9b5e450b811deb8897ffe78417 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Fri, 29 May 2020 19:59:22 +0200
Subject: proved a few oopses + minor tweaks

---
 hott/More_List.thy | 12 +-----------
 1 file changed, 1 insertion(+), 11 deletions(-)

(limited to 'hott/More_List.thy')

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