Safe Haskell	None
Language	Haskell2010

Agda.Syntax.Reflected

Documentation

type Args = [Arg Term] Source #

data Elim' a Source #

Constructors

Apply (Arg a)

Instances

Instances details

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 # show :: Elim' a -> String # showList :: [Elim' a] -> ShowS #
ToAbstract (Expr, Elims) Expr Source #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: MonadReflectedToAbstract m => (Expr, Elims) -> m Expr Source #
ToAbstract (Expr, Elim) Expr Source #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: MonadReflectedToAbstract m => (Expr, Elim) -> m Expr Source #

type Elim = Elim' Term Source #

type Elims = [Elim] Source #

argsToElims :: Args -> Elims Source #

data Abs a Source #

Constructors

Abs String a

Instances

Instances details

Show a => Show (Abs a) Source #
Instance details Defined in Agda.Syntax.Reflected Methods showsPrec :: Int -> Abs a -> ShowS # show :: Abs a -> String # showList :: [Abs a] -> ShowS #
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 :: MonadReflectedToAbstract m => Abs r -> m (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

Instances details

Show Term Source #
Instance details Defined in Agda.Syntax.Reflected Methods showsPrec :: Int -> Term -> ShowS # show :: Term -> String # showList :: [Term] -> ShowS #
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 :: MonadReflectedToAbstract m => Term -> m Expr Source #
ToAbstract [Arg Term] [NamedArg Expr] Source #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: MonadReflectedToAbstract m => [Arg Term] -> m [NamedArg Expr] Source #
ToAbstract (Expr, Elims) Expr Source #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: MonadReflectedToAbstract m => (Expr, Elims) -> m Expr Source #
ToAbstract (Expr, Elim) Expr Source #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: MonadReflectedToAbstract m => (Expr, Elim) -> m Expr Source #

type Type = Term Source #

data Sort Source #

Constructors

SetS Term
LitS Integer
UnknownS

Instances

Instances details

Show Sort Source #
Instance details Defined in Agda.Syntax.Reflected Methods showsPrec :: Int -> Sort -> ShowS # show :: Sort -> String # showList :: [Sort] -> ShowS #
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 :: MonadReflectedToAbstract m => Sort -> m Expr Source #

data Pattern Source #

Constructors

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

Instances

Instances details

Show Pattern Source #
Instance details Defined in Agda.Syntax.Reflected Methods showsPrec :: Int -> Pattern -> ShowS # show :: Pattern -> String # showList :: [Pattern] -> ShowS #
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 :: MonadReflectedToAbstract m => Pattern0 -> m (Names, Pattern) Source #

data Clause Source #

Constructors

Clause [Arg Pattern] Term
AbsurdClause [Arg Pattern]

Instances

Instances details

Show Clause Source #
Instance details Defined in Agda.Syntax.Reflected Methods showsPrec :: Int -> Clause -> ShowS # show :: Clause -> String # showList :: [Clause] -> ShowS #
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 :: MonadReflectedToAbstract m => QNamed Clause0 -> m Clause Source #
ToAbstract [QNamed Clause] [Clause] Source #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Methods toAbstract :: MonadReflectedToAbstract m => [QNamed Clause0] -> m [Clause] Source #

data Definition Source #

Constructors

FunDef Type [Clause]
DataDef
RecordDef
DataConstructor
Axiom
Primitive

Instances

Instances details

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