Agda-2.6.0.1: A dependently typed functional programming language and proof assistant

Safe Haskell | None
Language | Haskell2010

Agda.Syntax.Reflected

# Documentation

type Args = [Arg Term] Source #

data Elim' a Source #

Constructors

Apply (Arg a) |

Instances

Unquote Elim Source # |
Instance details Defined in Agda.TypeChecking.Unquote Methods unquote :: Term -> UnquoteM Elim Source #
Show a => Show (Elim' a) Source # |
Instance details Defined in Agda.Syntax.Reflected Methods showsPrec :: Int -> Elim' a -> ShowS Source # show :: Elim' a -> String Source # showList :: [Elim' a] -> ShowS Source #
ToAbstract (Expr, Elims) Expr Source # |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: (Expr, Elims) -> WithNames Expr Source #
ToAbstract (Expr, Elim) Expr Source # |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: (Expr, Elim) -> WithNames Expr Source #

type Elim = Elim' Term Source #

type Elims = [Elim] Source #

argsToElims :: Args -> Elims Source #

data Abs a Source #

Constructors

Abs String a |

Instances

Show a => Show (Abs a) Source # |
Instance details Defined in Agda.Syntax.Reflected Methods showsPrec :: Int -> Abs a -> ShowS Source # show :: Abs a -> String Source # showList :: [Abs a] -> ShowS Source #
Unquote a => Unquote (Abs a) Source # |
Instance details Defined in Agda.TypeChecking.Unquote Methods unquote :: Term -> UnquoteM (Abs a) Source #
ToAbstract r a => ToAbstract (Abs r) (a, Name) Source # |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: Abs r -> WithNames (a, Name) Source #

data Term Source #

Constructors

Var Int Elims |
Con QName Elims |
Def QName Elims |
Meta MetaId Elims |
Lam Hiding (Abs Term) |
ExtLam [Clause] Elims |
Pi (Dom Type) (Abs Type) |
Sort Sort |
Lit Literal |
Unknown |

Instances

Show Term Source # |
Instance details Defined in Agda.Syntax.Reflected Methods showsPrec :: Int -> Term -> ShowS Source # show :: Term -> String Source # showList :: [Term] -> ShowS Source #
PrettyTCM Term Source # |
Instance details Defined in Agda.TypeChecking.Pretty Methods prettyTCM :: Term -> TCM Doc Source #
Unquote Term Source # |
Instance details Defined in Agda.TypeChecking.Unquote Methods unquote :: Term0 -> UnquoteM Term Source #
Unquote Elim Source # |
Instance details Defined in Agda.TypeChecking.Unquote Methods unquote :: Term -> UnquoteM Elim Source #
ToAbstract Term Expr Source # |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: Term -> WithNames Expr Source #
ToAbstract [Arg Term] [NamedArg Expr] Source # |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: [Arg Term] -> WithNames [NamedArg Expr] Source #
ToAbstract (Expr, Elims) Expr Source # |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: (Expr, Elims) -> WithNames Expr Source #
ToAbstract (Expr, Elim) Expr Source # |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: (Expr, Elim) -> WithNames Expr Source #

type Type = Term Source #

data Sort Source #

Constructors

SetS Term |
LitS Integer |
UnknownS |

Instances

Show Sort Source # |
Instance details Defined in Agda.Syntax.Reflected Methods showsPrec :: Int -> Sort -> ShowS Source # show :: Sort -> String Source # showList :: [Sort] -> ShowS Source #
Unquote Sort Source # |
Instance details Defined in Agda.TypeChecking.Unquote Methods unquote :: Term -> UnquoteM Sort Source #
ToAbstract Sort Expr Source # |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: Sort -> WithNames Expr Source #

data Pattern Source #

Constructors

ConP QName [Arg Pattern] |
DotP |
VarP String |
LitP Literal |
AbsurdP |
ProjP QName |

Instances

Show Pattern Source # |
Instance details Defined in Agda.Syntax.Reflected Methods showsPrec :: Int -> Pattern -> ShowS Source # show :: Pattern -> String Source # showList :: [Pattern] -> ShowS Source #
Unquote Pattern Source # |
Instance details Defined in Agda.TypeChecking.Unquote Methods unquote :: Term -> UnquoteM Pattern Source #
ToAbstract Pattern (Names, Pattern) Source # |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: Pattern0 -> WithNames (Names, Pattern) Source #

data Clause Source #

Constructors

Clause [Arg Pattern] Term |
AbsurdClause [Arg Pattern] |

Instances

Show Clause Source # |
Instance details Defined in Agda.Syntax.Reflected Methods showsPrec :: Int -> Clause -> ShowS Source # show :: Clause -> String Source # showList :: [Clause] -> ShowS Source #
Unquote Clause Source # |
Instance details Defined in Agda.TypeChecking.Unquote Methods unquote :: Term -> UnquoteM Clause Source #
ToAbstract (QNamed Clause) Clause Source # |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: QNamed Clause0 -> WithNames Clause Source #
ToAbstract [QNamed Clause] [Clause] Source # |
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: [QNamed Clause0] -> WithNames [Clause] Source #

data Definition Source #

Constructors

FunDef Type [Clause] |
DataDef |
RecordDef |
DataConstructor |
Axiom |
Primitive |

Instances

Show Definition Source # |
Instance details Defined in Agda.Syntax.Reflected Methods showsPrec :: Int -> Definition -> ShowS Source # show :: Definition -> String Source # showList :: [Definition] -> ShowS Source #