 | Agda-2.2.6: A dependently typed functional programming language and proof assistant | Source code | Contents | Index |
| Agda.Syntax.Translation.InternalToAbstract |
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
| apps :: MonadTCM tcm => (Expr, [Arg Expr]) -> tcm Expr | Source |
| exprInfo :: ExprInfo | Source |
| reifyApp :: MonadTCM tcm => Expr -> [Arg Term] -> tcm Expr | Source |
| class Reify i a | i -> a where | Source |
| Methods | |||
|
| reifyDisplayForm :: MonadTCM tcm => QName -> Args -> tcm Expr -> tcm Expr | Source |
| reifyDisplayFormP :: LHS -> TCM LHS | Source |
| data NamedClause | Source |
| Constructors | ||
|
| stripImplicits :: MonadTCM tcm => [NamedArg Pattern] -> [Pattern] -> tcm ([NamedArg Pattern], [Pattern]) | Source |
| class DotVars a where | Source |
| Methods | |||
|
| reifyPatterns :: MonadTCM tcm => Telescope -> Permutation -> [Arg Pattern] -> tcm [NamedArg Pattern] | Source |