| Who Cites firstn? |
|
firstn | Def firstn(n;as)
Def == Case of as
Def == Canil nil
Def == Caa.as' if 0< n [a / firstn(n-1;as')] else nil fi
Def (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)  |