WhoCites Definitions mb label Sections GenAutomata Doc

Who Cites nth tl?
nth_tlDef nth_tl(n;as) == if n0 as else nth_tl(n-1;tl(as)) fi (recursive)
Thm* A:Type, as:A List, i:. nth_tl(i;as) A List
tl Def tl(l) == Case of l; nil nil ; h.t t
Thm* A:Type, l:A List. tl(l) A List
le_int Def ij == j < i
Thm* i,j:. (ij)
lt_int Def i < j == if i < j true ; false fi
Thm* i,j:. (i < j)
bnot Def b == if b false else true fi
Thm* b:. b

Syntax:nth_tl(n;as) has structure: nth_tl(n; as)

About:
listnillist_indboolbfalse
btrueifthenelseintnatural_numbersubtractless
recursive_def_noticeuniversememberall!abstraction

WhoCites Definitions mb label Sections GenAutomata Doc