| Some definitions of interest. |
|
his_num_rep | Def is_num_rep
Def == m: .  P:  
Def == m: .  ((P(zero_rep)) ( n: . (P(n))  (P(suc_rep(n)))))  (P(m)) |
| | Thm* is_num_rep (hind  hbool) |
|
assert | Def b == if b True else False fi |
| | Thm* b: . b Prop |
|
hrep_num | Def rep_num == n: . ncompose(suc_rep;n;zero_rep) |
| | Thm* rep_num (hnum  hind) |
|
label | Def t ...$L == t |
|
nat | Def == {i: | 0 i } |
| | Thm* Type |
| | Thm* S |