From 831f33468f227c0dc96bd31380236f2c77e70c52 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Thu, 9 Jul 2020 13:35:39 +0200
Subject: Non-annotated object lambda

---
 hott/More_List.thy | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'hott/More_List.thy')

diff --git a/hott/More_List.thy b/hott/More_List.thy
index a216987..460dc7b 100644
--- a/hott/More_List.thy
+++ b/hott/More_List.thy
@@ -7,7 +7,7 @@ begin
 
 section \<open>Length\<close>
 
-definition [implicit]: "len \<equiv> ListRec ? Nat 0 (\<lambda>_ _ rec. suc rec)"
+definition [implicit]: "len \<equiv> ListRec ? Nat 0 (fn _ _ rec. suc rec)"
 
 experiment begin
   Lemma "len [] \<equiv> ?n" by (subst comps)+
-- 
cgit v1.2.3