aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--hott/More_List.thy2
1 files changed, 1 insertions, 1 deletions
diff --git a/hott/More_List.thy b/hott/More_List.thy
index aa57635..c3d63f6 100644
--- a/hott/More_List.thy
+++ b/hott/More_List.thy
@@ -16,7 +16,7 @@ definition [implicit]:
"len \<equiv> ListRec ? Nat 0 (\<lambda>_ _ n. suc n)"
experiment begin
- Lemma "len [] \<equiv> 0" by reduce
+ Lemma "len [] \<equiv> ?n" by (subst comps)+
Lemma "len [0, suc 0, suc (suc 0)] \<equiv> ?n" by (subst comps)+
end