| Agda-2.2.6: A dependently typed functional programming language and proof assistant | Source code | Contents | Index

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 where | Source

Methods

reify :: MonadTCM tcm => i -> tcm a | Source

Instances

Reify Literal Expr
Reify Literal Expr
Reify MetaId Expr
Reify MetaId Expr
Reify ClauseBody RHS
Reify ClauseBody RHS
Reify Telescope Telescope
Reify Telescope Telescope
Reify Sort Expr
Reify Sort Expr
Reify Type Expr
Reify Type Expr
Reify Term Expr
Reify Term Expr
Reify DisplayTerm Expr
Reify DisplayTerm Expr
Reify NamedClause Clause
Reify NamedClause Clause
Reify Constraint (OutputForm Expr Expr)
Reify Constraint (OutputForm Expr Expr)
Reify i a => Reify ([] i) ([] a)
Reify i a => Reify (Arg i) (Arg a)
Reify i a => Reify (Abs i) ((,) Name a)
Reify i a => Reify (Abs i) ((,) Name a)
(Reify i1 a1, Reify i2 a2) => Reify ((,) i1 i2) ((,) a1 a2)
(Reify t t', Reify a a') => Reify (Judgement t a) (Judgement t' a')

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

reifyDisplayFormP :: LHS -> TCM LHS | Source

data NamedClause | Source

Constructors

NamedClause QName Clause |

Instances

Reify NamedClause Clause

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

class DotVars a where | Source

Methods

dotVars :: a -> Set Name | Source

Instances

DotVars Pattern
DotVars TypedBinding
DotVars TypedBindings
DotVars Expr
DotVars a => DotVars ([] a)
DotVars a => DotVars (Arg a)
(DotVars a, DotVars b) => DotVars ((,) a b)
DotVars a => DotVars (Named s a)

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

Produced by Haddock version 2.4.2