Agda-2.3.0: 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

Synopsis

Documentation

class DotVars a whereSource

dotVars ps gives all the variables inside of dot patterns of ps It is only invoked for patternish things. (Ulf O-tone!) Use it for printing l.h.sides: which of the implicit arguments have to be made explicit.

Methods

dotVars :: a -> Set NameSource

Instances

DotVars Pattern 
DotVars RHS 
DotVars Clause 
DotVars TypedBinding 
DotVars TypedBindings 
DotVars Expr

Getting all(!) variables of an expression. It should only get free ones, but it does not matter to include the bound ones.

DotVars a => DotVars [a] 
DotVars a => DotVars (Arg a) 
(DotVars a, DotVars b) => DotVars (a, b) 
DotVars a => DotVars (Named s a)