blob: dc523206b72df930db2cf16bfdef8561c9f4ea09 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
|
theory List_HoTT
imports
MLTT.List
Nat
begin
section \<open>Length\<close>
definition [implicit]: "len \<equiv> ListRec {} Nat 0 (fn _ _ rec. suc rec)"
experiment begin
Lemma "len [] \<equiv> ?n" by (subst comp; typechk?)+
Lemma "len [0, suc 0, suc (suc 0)] \<equiv> ?n" by (subst comp; typechk?)+
end
end
|