aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorJosh Chen2020-05-29 10:20:36 +0200
committerJosh Chen2020-05-29 10:20:36 +0200
commit41da54eca527b7c61f13ebcb75a8970bc845bb40 (patch)
treef5ee5fad3b514eb97dac2db061bc47c523849b9e
parent417af1adf5453720c55e27de212b830569311f0e (diff)
minor
-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