}
A:Type, n:. A List(n) Type
0 ; a.as' ||as'||+1 (recursive)A:Type, l:A List. ||l|| | Who Cites list n? | |
| list_n | Def A List(n) == {x:(A List)| ||x|| = n } |
| Thm* A:Type, n:. A List(n) Type | |
| length | Def ||as|| == Case of as; nil 0 ; a.as' ||as'||+1 (recursive) |
| Thm* A:Type, l:A List. ||l|| | |
| Thm* ||nil|| |
| Syntax: | A List(n) | has structure: | list_n(A; n) |
About:
 |  |  |  |  |  |
 |  |  |  |  |  |
 |