Safe Haskell	None
Language	Haskell98

Agda.Syntax.Translation.InternalToAbstract

Description

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

TODO

Documentation

class Reify i a | i -> a where Source

Minimal complete definition

Methods

Instances

Reify Name Name Source
Reify Literal Expr Source
Reify Expr Expr Source
Reify ClauseBody RHS Source
Reify MetaId Expr Source
Reify Level Expr Source
Reify Sort Expr Source
Reify Telescope Telescope Source
Reify Type Expr Source
Reify Elim Expr Source
Reify Term Expr Source
Reify ArgInfo ArgInfo Source
Reify DisplayTerm Expr Source
Reify NamedClause Clause Source
Reify i a => Reify [i] [a] Source
Reify i a => Reify (Dom i) (Arg a) Source
Reify i a => Reify (Arg i) (Arg a) Source	Skip reification of implicit and irrelevant args if option is off.
(Free i, Reify i a) => Reify (Abs i) (Name, a) Source
(Reify i1 a1, Reify i2 a2) => Reify (i1, i2) (a1, a2) Source
Reify i a => Reify (Named n i) (Named n a) Source
(Reify i1 a1, Reify i2 a2, Reify i3 a3) => Reify (i1, i2, i3) (a1, a2, a3) Source
(Reify i1 a1, Reify i2 a2, Reify i3 a3, Reify i4 a4) => Reify (i1, i2, i3, i4) (a1, a2, a3, a4) Source