hott/More_List.thy


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18

theory More_List
imports
  Spartan.List
  Nat

begin

section ‹Length›

definition [implicit]: "len ≡ ListRec ? Nat 0 (fn _ _ rec. suc rec)"

experiment begin
  Lemma "len [] ≡ ?n" by (subst comp)+
  Lemma "len [0, suc 0, suc (suc 0)] ≡ ?n" by (subst comp)+
end


end