Safe Haskell | None |
---|
Translating from internal syntax to abstract syntax. Enables nice pretty printing of internal syntax.
TODO
- numbers on metas - fake dependent functions to independent functions - meta parameters - shadowing
Documentation
class Reify i a | i -> a whereSource
Reify Literal Expr | |
Reify ClauseBody RHS | |
Reify MetaId Expr | |
Reify Level Expr | |
Reify Sort Expr | |
Reify Telescope Telescope | |
Reify Type Expr | |
Reify Elim Expr | |
Reify Term Expr | |
Reify Expr Expr | |
Reify DisplayTerm Expr | |
Reify NamedClause Clause | |
Reify ProblemConstraint (Closure (OutputForm Expr Expr)) | |
Reify Constraint (OutputConstraint Expr Expr) | |
Reify i a => Reify [i] [a] | |
ReifyWhen i a => Reify (Arg i) (Arg a) | Skip reification of implicit and irrelevant args if option is off. |
Reify i a => Reify (Dom i) (Arg a) | |
(Free i, Reify i a) => Reify (Abs i) (Name, a) | |
(Reify i1 a1, Reify i2 a2) => Reify (i1, i2) (a1, a2) | |
Reify i a => Reify (Named n i) (Named n a) | |
(Reify t t', Reify a a') => Reify (Judgement t a) (Judgement t' a') |
class Reify i a => ReifyWhen i a whereSource
ReifyWhen
is a auxiliary type class to reify Arg
.
reifyWhen False
should produce an underscore
.
This function serves to reify hidden/irrelevant things.
type NamedClause = QNamed ClauseSource
reifyPatterns :: Telescope -> Permutation -> [Arg Pattern] -> TCM [NamedArg Pattern]Source