Agda-2.2.10: A dependently typed functional programming language and proof assistant

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

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 whereSource

Methods

reify :: MonadTCM tcm => i -> tcm aSource

reifyDisplayForm :: MonadTCM tcm => QName -> Args -> tcm Expr -> tcm Expr Source

reifyDisplayFormP :: LHS -> TCM LHS Source

data NamedClause Source

Constructors

NamedClause QName Clause

stripImplicits :: MonadTCM tcm => [NamedArg Pattern] -> [Pattern] -> tcm ([NamedArg Pattern], [Pattern])Source

class DotVars a whereSource

Methods

dotVars :: a -> Set Name Source

reifyPatterns :: MonadTCM tcm => Telescope -> Permutation -> [Arg Pattern] -> tcm [NamedArg Pattern]Source