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

reifyApp :: MonadTCM tcm => Expr -> [Arg Term] -> tcm Expr

class Reify i a | i -> a where

Methods

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

Instances

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

class DotVars a where

Methods

dotVars :: a -> Set Name