20 lines
494 B
Text
20 lines
494 B
Text
(term.pi{1}
|
|
"Π"
|
|
(term.binders (0 (term.binders_ext [(term.binder_ident (0 `a))] [])))
|
|
","
|
|
(term.sort (1 "Type")))
|
|
(term.pi{2}
|
|
"Π"
|
|
(term.binders{1} (0 (term.binders_ext [(term.binder_ident (0 `a))] [])))
|
|
","
|
|
(term.sort{1} (1 "Type")))
|
|
(term.pi{2, 1}
|
|
"Π"
|
|
(term.binders{1} (0 (term.binders_ext [(term.binder_ident (0 `a))] [])))
|
|
","
|
|
(term.sort{1} (1 "Type")))
|
|
(term.pi
|
|
"Π"
|
|
(term.binders{2} (0 (term.binders_ext [(term.binder_ident (0 `a))] [])))
|
|
","
|
|
(term.sort{2} (1 "Type")))
|