Agda-2.2.6: A dependently typed functional programming language and proof assistantSource codeContentsIndex
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 ExprSource
exprInfo :: ExprInfoSource
reifyApp :: MonadTCM tcm => Expr -> [Arg Term] -> tcm ExprSource
class Reify i a | i -> a whereSource
Methods
reify :: MonadTCM tcm => i -> tcm aSource
show/hide Instances
reifyDisplayForm :: MonadTCM tcm => QName -> Args -> tcm Expr -> tcm ExprSource
reifyDisplayFormP :: LHS -> TCM LHSSource
data NamedClause Source
Constructors
NamedClause QName Clause
show/hide Instances
stripImplicits :: MonadTCM tcm => [NamedArg Pattern] -> [Pattern] -> tcm ([NamedArg Pattern], [Pattern])Source
class DotVars a whereSource
Methods
dotVars :: a -> Set NameSource
show/hide Instances
reifyPatterns :: MonadTCM tcm => Telescope -> Permutation -> [Arg Pattern] -> tcm [NamedArg Pattern]Source
Produced by Haddock version 2.4.2