Agda- A dependently typed functional programming language and proof assistant

Safe HaskellNone



Translating from internal syntax to abstract syntax. Enables nice pretty printing of internal syntax.


  • numbers on metas - fake dependent functions to independent functions - meta parameters - shadowing



class Reify i a | i -> a whereSource


reify :: i -> TCM aSource


Reify Literal Expr 
Reify ClauseBody RHS 
Reify MetaId Expr 
Reify Level Expr 
Reify Sort Expr 
Reify Telescope Telescope 
Reify Type Expr 
Reify Elim Expr 
Reify Term Expr 
Reify Expr Expr 
Reify DisplayTerm Expr 
Reify NamedClause Clause 
Reify ProblemConstraint (Closure (OutputForm Expr Expr)) 
Reify Constraint (OutputConstraint Expr Expr) 
Reify i a => Reify [i] [a] 
ReifyWhen i a => Reify (Arg i) (Arg a)

Skip reification of implicit and irrelevant args if option is off.

Reify i a => Reify (Dom i) (Arg a) 
(Free i, Reify i a) => Reify (Abs i) (Name, a) 
(Reify i1 a1, Reify i2 a2) => Reify (i1, i2) (a1, a2) 
Reify i a => Reify (Named n i) (Named n a) 
(Reify t t', Reify a a') => Reify (Judgement t a) (Judgement t' a') 

class Reify i a => ReifyWhen i a whereSource

ReifyWhen is a auxiliary type class to reify Arg.

reifyWhen False should produce an underscore. This function serves to reify hidden/irrelevant things.


reifyWhen :: Bool -> i -> TCM aSource


Reify i Expr => ReifyWhen i Expr 
ReifyWhen i a => ReifyWhen (Arg i) (Arg a) 
ReifyWhen i a => ReifyWhen (Named n i) (Named n a)