Reify MetaId Expr Source # | |
Instance detailsDefined in Agda.Syntax.Translation.InternalToAbstract |
Reify Name Name Source # | |
Instance detailsDefined in Agda.Syntax.Translation.InternalToAbstract |
Reify Literal Expr Source # | |
Instance detailsDefined in Agda.Syntax.Translation.InternalToAbstract |
Reify Level Expr Source # | |
Instance detailsDefined in Agda.Syntax.Translation.InternalToAbstract |
Reify Sort Expr Source # | |
Instance detailsDefined in Agda.Syntax.Translation.InternalToAbstract |
Reify Telescope Telescope Source # | |
Instance detailsDefined in Agda.Syntax.Translation.InternalToAbstract |
Reify Type Expr Source # | |
Instance detailsDefined in Agda.Syntax.Translation.InternalToAbstract |
Reify Term Expr Source # | |
Instance detailsDefined in Agda.Syntax.Translation.InternalToAbstract |
Reify Expr Expr Source # | |
Instance detailsDefined in Agda.Syntax.Translation.InternalToAbstract |
Reify DisplayTerm Expr Source # | |
Instance detailsDefined in Agda.Syntax.Translation.InternalToAbstract |
Reify NamedClause Clause Source # | |
Instance detailsDefined in Agda.Syntax.Translation.InternalToAbstract |
Reify ProblemConstraint (Closure (OutputForm Expr Expr)) Source # | |
Instance detailsDefined in Agda.Interaction.BasicOps |
Reify Constraint (OutputConstraint Expr Expr) Source # | |
Instance detailsDefined in Agda.Interaction.BasicOps |
Reify (QNamed Clause) Clause Source # | |
Instance detailsDefined in Agda.Syntax.Translation.InternalToAbstract |
Reify i a => Reify [i] [a] Source # | |
Instance detailsDefined in Agda.Syntax.Translation.InternalToAbstract |
Reify i a => Reify (Dom i) (Arg a) Source # | |
Instance detailsDefined in Agda.Syntax.Translation.InternalToAbstract |
Reify i a => Reify (Arg i) (Arg a) Source # | Skip reification of implicit and irrelevant args if option is off. |
Instance detailsDefined in Agda.Syntax.Translation.InternalToAbstract |
Reify (QNamed System) [Clause] Source # | |
Instance detailsDefined in Agda.Syntax.Translation.InternalToAbstract |
Reify i a => Reify (Elim' i) (Elim' a) Source # | |
Instance detailsDefined in Agda.Syntax.Translation.InternalToAbstract |
(Free i, Reify i a) => Reify (Abs i) (Name, a) Source # | |
Instance detailsDefined in Agda.Syntax.Translation.InternalToAbstract |
(Reify i1 a1, Reify i2 a2) => Reify (i1, i2) (a1, a2) Source # | |
Instance detailsDefined in Agda.Syntax.Translation.InternalToAbstract |
Reify i a => Reify (Named n i) (Named n a) Source # | |
Instance detailsDefined in Agda.Syntax.Translation.InternalToAbstract |
(Reify i1 a1, Reify i2 a2, Reify i3 a3) => Reify (i1, i2, i3) (a1, a2, a3) Source # | |
Instance detailsDefined in Agda.Syntax.Translation.InternalToAbstract |
(Reify i1 a1, Reify i2 a2, Reify i3 a3, Reify i4 a4) => Reify (i1, i2, i3, i4) (a1, a2, a3, a4) Source # | |
Instance detailsDefined in Agda.Syntax.Translation.InternalToAbstract Methods reify :: (i1, i2, i3, i4) -> TCM (a1, a2, a3, a4) Source # reifyWhen :: Bool -> (i1, i2, i3, i4) -> TCM (a1, a2, a3, a4) Source # |