89 lines
2 KiB
Text
89 lines
2 KiB
Text
=====
|
|
Sorts
|
|
=====
|
|
|
|
def foo (A : ★) (B : □) (C : □₁) (D : []) (E : []1) (F : □1) (G : □₁₂₃) (H : ⋆) := A;
|
|
|
|
---
|
|
|
|
(program
|
|
(definition
|
|
(identifier)
|
|
(param_block
|
|
(identifier)
|
|
(expr
|
|
(app_term
|
|
(binex
|
|
(app
|
|
(term
|
|
(sort
|
|
(star))))))))
|
|
(param_block
|
|
(identifier)
|
|
(expr
|
|
(app_term
|
|
(binex
|
|
(app
|
|
(term
|
|
(sort
|
|
(square))))))))
|
|
(param_block
|
|
(identifier)
|
|
(expr
|
|
(app_term
|
|
(binex
|
|
(app
|
|
(term
|
|
(sort
|
|
(square))))))))
|
|
(param_block
|
|
(identifier)
|
|
(expr
|
|
(app_term
|
|
(binex
|
|
(app
|
|
(term
|
|
(sort
|
|
(square))))))))
|
|
(param_block
|
|
(identifier)
|
|
(expr
|
|
(app_term
|
|
(binex
|
|
(app
|
|
(term
|
|
(sort
|
|
(square))))))))
|
|
(param_block
|
|
(identifier)
|
|
(expr
|
|
(app_term
|
|
(binex
|
|
(app
|
|
(term
|
|
(sort
|
|
(square))))))))
|
|
(param_block
|
|
(identifier)
|
|
(expr
|
|
(app_term
|
|
(binex
|
|
(app
|
|
(term
|
|
(sort
|
|
(square))))))))
|
|
(param_block
|
|
(identifier)
|
|
(expr
|
|
(app_term
|
|
(binex
|
|
(app
|
|
(term
|
|
(sort
|
|
(star))))))))
|
|
(expr
|
|
(app_term
|
|
(binex
|
|
(app
|
|
(term
|
|
(identifier))))))))
|