Nuprl - Some Definitions

Thms exponent Sections AutomataTheory Doc

NOTE: (f)[

n] is just listify(f; 0; n).

listify Def listify(f; m; n) == if nm nil else f(m).listify(f; m+1; n) fi (recursive)
Thm* T:Type, m,n:, f:({m..n}T). listify(f; m; n) T*

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

About:

listify	`Def listify(f; m; n) == if nm nil else f(m).listify(f; m+1; n) fi (recursive)` `Thm* T:Type, m,n:, f:({m..n}T). listify(f; m; n) T*`
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`