b == if b
True else False fib == if b True else False fiis mentioned by
 n: . odd(n)   ( m:. n = 2 m+1  ) | [odd_exists] |
| n:. even(n) (m:. n = 2m ) | [even_exists] |
n:. (even(n)  (m:. n = 2m )) & (odd(n) (m:. n = 2m+1 )) | [even_odd_exists] |
| n:. odd(2n+1) | [odd_double] |
| n:. even(2n) | [even_double] |
| m,n:. odd(mn) odd(m) & odd(n) | [odd_mult] |
m,n:. odd(m+n)  (odd(m) odd(n)) | [odd_add] |
m,n:. even(mn) even(m)  even(n) | [even_mult] |
| m,n:. even(m+n) (even(m) even(n)) | [even_add] |
| n:. (even(n) & odd(n)) | [even_and_odd] |
| n:. even(n) odd(n) | [even_or_odd] |
| n:. odd(n) even(n) | [odd_even] |
| n:. even(n) odd(n) | [even_odd] |
In prior sections: bool 1 hol hol bool hol num hol prim rec hol arithmetic 2 hol arithmetic 4 hol min
Try larger context:
HOLlib
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html