nil ; a.as' if 0 < 
n [a / firstn(n-1;as')] else nil fi (recursive)
A:Type, as:A List, n:
. firstn(n;as) 
A Listj == if i < j true ; false fii,j:. (i < j) 
| Who Cites firstn? | |
| firstn | Def firstn(n;as) == Case of as; nil nil ; a.as' if 0 < n [a / firstn(n-1;as')] else nil fi (recursive) |
| Thm* A:Type, as:A List, n:. firstn(n;as) A List | |
| lt_int | Def i < j == if i < j true ; false fi |
| Thm* i,j:. (i < j) |
| Syntax: | firstn(n;as) | has structure: | firstn(n; as) |
About:
 |  |  |  |  |
 |  |  |  |  |  |
 |  |  |  |  |
 |