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