Who Cites reject? | |
reject | Def as\[i] == if i0 tl(as) else Case of as; nil nil ; a'.as' [a' / as'\[i-1]] fi (recursive) |
Thm* A:Type, l:A List, n:. l\[n] 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: | as\[i] | has structure: | reject(i; as) |
About: