fcdbdeecaf
/cc @leodemoura it's not bullet-proof (unless `pp.explicit` is set), but let's see if it is good enough in practice
102 lines
4.1 KiB
Text
102 lines
4.1 KiB
Text
(Term.prop "Prop")
|
||
(Term.type "Type")
|
||
(Term.type "Type")
|
||
(Term.sortApp (Term.type "Type") (Level.num (numLit "1")))
|
||
(Term.sortApp (Term.type "Type") (Level.hole "_"))
|
||
(Term.sortApp (Term.type "Type") (Level.addLit (Level.hole "_") "+" (numLit "2")))
|
||
(Term.id `Nat (null))
|
||
(Term.app (Term.id `List (null)) (null (Term.id `Nat (null))))
|
||
(Term.app (Term.id `id (null)) (null (Term.id `Nat (null))))
|
||
(Term.app (Term.id `List (null)) (null (Term.id `Nat (null))))
|
||
(Term.app (Term.explicit "@" (Term.id `id (null))) (null (Term.type "Type") (Term.id `Nat (null))))
|
||
(Term.app
|
||
(Term.id `List (null (Term.explicitUniv ".{" (null (Level.num (numLit "0"))) "}")))
|
||
(null (Term.id `Nat (null))))
|
||
(Term.app
|
||
(Term.id `id (null (Term.explicitUniv ".{" (null (Level.num (numLit "2"))) "}")))
|
||
(null (Term.id `Nat (null))))
|
||
(Term.app
|
||
(Term.id `id (null))
|
||
(null (Term.app (Term.explicit "@" (Term.id `id (null))) (null (Term.type "Type") (Term.id `Nat (null))))))
|
||
(Term.fun
|
||
"fun"
|
||
(null (Term.paren "(" (null (Term.id `a (null)) (null (Term.typeAscription ":" (Term.id `Nat (null))))) ")"))
|
||
"=>"
|
||
(Term.id `a (null)))
|
||
(Term.fun
|
||
"fun"
|
||
(null
|
||
(Term.paren
|
||
"("
|
||
(null (Term.app (Term.id `a (null)) (null (Term.id `b (null)))) (null (Term.typeAscription ":" (Term.id `Nat (null)))))
|
||
")"))
|
||
"=>"
|
||
(Term.id `a (null)))
|
||
(Term.fun
|
||
"fun"
|
||
(null
|
||
(Term.paren "(" (null (Term.id `a (null)) (null (Term.typeAscription ":" (Term.id `Nat (null))))) ")")
|
||
(Term.paren "(" (null (Term.id `b (null)) (null (Term.typeAscription ":" (Term.id `Bool (null))))) ")"))
|
||
"=>"
|
||
(Term.id `a (null)))
|
||
(Term.fun
|
||
"fun"
|
||
(null (Term.implicitBinder "{" (null `a `b) (null ":" (Term.id `Nat (null))) "}"))
|
||
"=>"
|
||
(Term.id `a (null)))
|
||
(Term.app
|
||
(Term.id `typeAs (null))
|
||
(null
|
||
(Term.depArrow
|
||
(Term.implicitBinder "{" (null `α) (null ":" (Term.type "Type")) "}")
|
||
"→"
|
||
(Term.arrow (Term.id `α (null)) "→" (Term.id `α (null))))
|
||
(Term.fun
|
||
"fun"
|
||
(null
|
||
(Term.implicitBinder "{" (null `α) (null ":" (Term.type "Type")) "}")
|
||
(Term.paren "(" (null (Term.id `a (null)) (null (Term.typeAscription ":" (Term.id `α (null))))) ")"))
|
||
"=>"
|
||
(Term.id `a (null)))))
|
||
(Term.fun
|
||
"fun"
|
||
(null
|
||
(Term.implicitBinder "{" (null `α) (null ":" (Term.type "Type")) "}")
|
||
(Term.instBinder "[" (null `_inst_1 ":") (Term.app (Term.id `HasToString (null)) (null (Term.id `α (null)))) "]")
|
||
(Term.paren "(" (null (Term.id `a (null)) (null (Term.typeAscription ":" (Term.id `α (null))))) ")"))
|
||
"=>"
|
||
(Term.app
|
||
(Term.explicit "@" (Term.id `HasToString.toString (null)))
|
||
(null (Term.id `α (null)) (Term.id `_inst_1 (null)) (Term.id `a (null)))))
|
||
(Term.depArrow (Term.explicitBinder "(" (null `α) (null ":" (Term.type "Type")) (null) ")") "→" (Term.id `α (null)))
|
||
(Term.depArrow (Term.explicitBinder "(" (null `α `β) (null ":" (Term.type "Type")) (null) ")") "→" (Term.id `α (null)))
|
||
(Term.arrow (Term.type "Type") "→" (Term.arrow (Term.type "Type") "→" (Term.type "Type")))
|
||
(Term.depArrow
|
||
(Term.explicitBinder "(" (null `α) (null ":" (Term.type "Type")) (null) ")")
|
||
"→"
|
||
(Term.arrow (Term.id `α (null)) "→" (Term.id `α (null))))
|
||
(Term.depArrow
|
||
(Term.explicitBinder "(" (null `α) (null ":" (Term.type "Type")) (null) ")")
|
||
"→"
|
||
(Term.depArrow
|
||
(Term.explicitBinder "(" (null `a) (null ":" (Term.id `α (null))) (null) ")")
|
||
"→"
|
||
(Term.app (Term.id `Eq (null)) (null (Term.id `a (null)) (Term.id `a (null))))))
|
||
(Term.depArrow (Term.implicitBinder "{" (null `α) (null ":" (Term.type "Type")) "}") "→" (Term.id `α (null)))
|
||
(Term.depArrow
|
||
(Term.implicitBinder "{" (null `α) (null ":" (Term.type "Type")) "}")
|
||
"→"
|
||
(Term.depArrow
|
||
(Term.instBinder "[" (null `_inst_1 ":") (Term.app (Term.id `HasToString (null)) (null (Term.id `α (null)))) "]")
|
||
"→"
|
||
(Term.id `α (null))))
|
||
(Term.num (numLit "0"))
|
||
(Term.num (numLit "1"))
|
||
(Term.num (numLit "42"))
|
||
(Term.str (strLit "\"hi\""))
|
||
(Term.proj (Term.app (Term.id `Prod.mk (null)) (null (Term.num (numLit "1")) (Term.num (numLit "2")))) "." `fst)
|
||
(Term.app
|
||
(Term.id `or (null))
|
||
(null
|
||
(Term.app (Term.id `HasLess.Less (null)) (null (Term.num (numLit "1")) (Term.num (numLit "2"))))
|
||
(Term.id `Bool.true (null))))
|