else (p(head(l)))
every(p;tl(l)) fi
Def (recursive)
'a:Type, p:('a
), l:'a List. every(p;l) 
q == if p
q else false fip,q:. (pq) 
x:T. True } Type{2}| Some definitions of interest. | |
| every | else (p(head(l)))every(p;tl(l)) fi
Def (recursive) |
| 'a:Type, p:('a), l:'a List. every(p;l) | |
| band | q == if p q else false fi |
| p,q:. (pq) | |
| stype | x:T. True } |
| Type{2} |
About:
 |  |  |  |  |  |  |  |
 |  |  |  |  |  |  |