Definitions graph 1 2 Sections Graphs Doc

Some definitions of interest.
list-dec Def L[i--] == mklist(||L||;j.if j=i L[j]-1 else L[j] fi)
mklist Def mklist(n;f) == primrec(n;nil;i,l. l @ [(f(i))])
Thm* T:Type, n:, f:(nT). mklist(n;f) T List
eq_int Def i=j == if i=j true ; false fi
Thm* i,j:. (i=j)
int_seg Def {i..j} == {k:| i k < j }
Thm* m,n:. {m..n} Type
length Def ||as|| == Case of as; nil 0 ; a.as' ||as'||+1 (recursive)
Thm* A:Type, l:A List. ||l||
Thm* ||nil||
nat Def == {i:| 0i }
Thm* Type
select Def l[i] == hd(nth_tl(i;l))
Thm* A:Type, l:A List, n:. 0n n < ||l|| l[n] A

About:
listconsnillist_indboolbfalsebtrue
ifthenelseintnatural_numberaddsubtractint_eqless_thanset
lambdaapplyfunctionrecursive_def_noticeuniversememberimpliesall
!abstraction

Definitions graph 1 2 Sections Graphs Doc