aboutsummaryrefslogtreecommitdiff
path: root/hott/List+.thy
blob: b73cc24ab95495cb5f6d8d009ed960d04bc895c3 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
theory "List+"
imports
  Spartan.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)
  Lemma "len [0, suc 0, suc (suc 0)] \<equiv> ?n" by (subst comp)
end


end