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 MetaId Expr

Reify ClauseBody RHS

Reify Telescope Telescope

Reify Sort Expr

Reify Type Expr

Reify Term Expr

Reify DisplayTerm Expr

Reify NamedClause Clause

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 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]

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