IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def true
== inl(
)
is mentioned by
Def is_list_rep
Def == r:(  'a) .  f:  'a
Def == r:(  'a) .    n:
Def == r:(  'a) .    (r
Def == r:(  'a) .    = < m: . if m< n then f(m) else @ x:'a. true fi ,n>) | [his_list_rep] |
Def every(p;l) == if null(l) then true else (p(head(l))) every(p;tl(l)) fi
Def (recursive) | [every] |
In prior sections:
bool 1
hol
hol bool
hol arithmetic 1
list 1
Try larger context:
HOLlib
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html