| Safe Haskell | None |
|---|
Agda.Syntax.Translation.InternalToAbstract
Description
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 where
Instances
| 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 where
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 Clause
reifyPatterns :: Telescope -> Permutation -> [Arg Pattern] -> TCM [NamedArg Pattern]