Def == Case of as; nil
nil ; a.as' if 0<
n a.firstn(n-1;as') else nil fi
Def (recursive)
A:Type, as:A List, n:
. firstn(n;as) 
A List
B == 
B<Ai,j:. (ij) Propj == if i<j true ; false fii,j:. (i<j) 
| Some definitions of interest. | |
| firstn | Def == Case of as; nil nil ; a.as' if 0<n a.firstn(n-1;as') else nil fi
Def (recursive) |
| A:Type, as:A List, n:. firstn(n;as) A List | |
| le | B == B<A |
| i,j:. (ij) Prop | |
| lt_int | j == if i<j true ; false fi |
| i,j:. (i<j) |
About:
 |  |  |  |  |
 |  |  |  |  |  |  |
 |  |  |  |  |  |  |