Safe Haskell	Safe-Inferred
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, Elim) Source #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Associated Types type AbsOfRef (Expr, Elim) Source # Methods toAbstract :: MonadReflectedToAbstract m => (Expr, Elim) -> m (AbsOfRef (Expr, Elim)) Source #
ToAbstract (Expr, Elims) Source #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Associated Types type AbsOfRef (Expr, Elims) Source # Methods toAbstract :: MonadReflectedToAbstract m => (Expr, Elims) -> m (AbsOfRef (Expr, Elims)) Source #
type AbsOfRef (Expr, Elim) Source #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract type AbsOfRef (Expr, Elim) = Expr
type AbsOfRef (Expr, Elims) Source #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract type AbsOfRef (Expr, Elims) = Expr

type Elim = Elim' Term Source #

type Elims = [Elim] Source #

argsToElims :: Args -> Elims Source #

data Abs a Source #

Constructors

Abs String a

Instances

Instances details

ToAbstract r => ToAbstract (Abs r) Source #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Associated Types type AbsOfRef (Abs r) Source # Methods toAbstract :: MonadReflectedToAbstract m => Abs r -> m (AbsOfRef (Abs r)) Source #
Unquote a => Unquote (Abs a) Source #
Instance details Defined in Agda.TypeChecking.Unquote Methods unquote :: Term -> UnquoteM (Abs a) Source #
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 #
type AbsOfRef (Abs r) Source #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract type AbsOfRef (Abs r) = (AbsOfRef r, Name)

data Term Source #

Constructors

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

Instances

Instances details

ToAbstract Term Source #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Associated Types type AbsOfRef Term Source # Methods toAbstract :: MonadReflectedToAbstract m => Term -> m (AbsOfRef Term) Source #
Unquote Elim Source #
Instance details Defined in Agda.TypeChecking.Unquote Methods unquote :: Term -> UnquoteM Elim Source #
Unquote Term Source #
Instance details Defined in Agda.TypeChecking.Unquote Methods unquote :: Term0 -> UnquoteM Term Source #
Show Term Source #
Instance details Defined in Agda.Syntax.Reflected Methods showsPrec :: Int -> Term -> ShowS # show :: Term -> String # showList :: [Term] -> ShowS #
ToAbstract (Expr, Elim) Source #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Associated Types type AbsOfRef (Expr, Elim) Source # Methods toAbstract :: MonadReflectedToAbstract m => (Expr, Elim) -> m (AbsOfRef (Expr, Elim)) Source #
ToAbstract (Expr, Elims) Source #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Associated Types type AbsOfRef (Expr, Elims) Source # Methods toAbstract :: MonadReflectedToAbstract m => (Expr, Elims) -> m (AbsOfRef (Expr, Elims)) Source #
type AbsOfRef Term Source #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract type AbsOfRef Term = Expr
type AbsOfRef (Expr, Elim) Source #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract type AbsOfRef (Expr, Elim) = Expr
type AbsOfRef (Expr, Elims) Source #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract type AbsOfRef (Expr, Elims) = Expr

type Type = Term Source #

data Sort Source #

Constructors

SetS Term
LitS Integer
PropS Term
PropLitS Integer
InfS Integer
UnknownS

Instances

Instances details

ToAbstract Sort Source #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Associated Types type AbsOfRef Sort Source # Methods toAbstract :: MonadReflectedToAbstract m => Sort -> m (AbsOfRef Sort) Source #
Unquote Sort Source #
Instance details Defined in Agda.TypeChecking.Unquote Methods unquote :: Term -> UnquoteM Sort Source #
Show Sort Source #
Instance details Defined in Agda.Syntax.Reflected Methods showsPrec :: Int -> Sort -> ShowS # show :: Sort -> String # showList :: [Sort] -> ShowS #
type AbsOfRef Sort Source #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract type AbsOfRef Sort = Expr

data Pattern Source #

Constructors

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

Instances

Instances details

ToAbstract Pattern Source #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Associated Types type AbsOfRef Pattern Source # Methods toAbstract :: MonadReflectedToAbstract m => Pattern -> m (AbsOfRef Pattern) Source #
Unquote Pattern Source #
Instance details Defined in Agda.TypeChecking.Unquote Methods unquote :: Term -> UnquoteM Pattern Source #
Show Pattern Source #
Instance details Defined in Agda.Syntax.Reflected Methods showsPrec :: Int -> Pattern -> ShowS # show :: Pattern -> String # showList :: [Pattern] -> ShowS #
type AbsOfRef Pattern Source #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract type AbsOfRef Pattern = Pattern

data Clause Source #

Constructors

Clause
Fields clauseTel :: [(Text, Arg Type)] clausePats :: [Arg Pattern] clauseRHS :: Term
AbsurdClause
Fields clauseTel :: [(Text, Arg Type)] clausePats :: [Arg Pattern]

Instances

Instances details

Unquote Clause Source #
Instance details Defined in Agda.TypeChecking.Unquote Methods unquote :: Term -> UnquoteM Clause Source #
Show Clause Source #
Instance details Defined in Agda.Syntax.Reflected Methods showsPrec :: Int -> Clause -> ShowS # show :: Clause -> String # showList :: [Clause] -> ShowS #
ToAbstract (QNamed Clause) Source #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Associated Types type AbsOfRef (QNamed Clause) Source # Methods toAbstract :: MonadReflectedToAbstract m => QNamed Clause -> m (AbsOfRef (QNamed Clause)) Source #
ToAbstract (List1 (QNamed Clause)) Source #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Associated Types type AbsOfRef (List1 (QNamed Clause)) Source # Methods toAbstract :: MonadReflectedToAbstract m => List1 (QNamed Clause) -> m (AbsOfRef (List1 (QNamed Clause))) Source #
ToAbstract [QNamed Clause] Source #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract Associated Types type AbsOfRef [QNamed Clause] Source # Methods toAbstract :: MonadReflectedToAbstract m => [QNamed Clause] -> m (AbsOfRef [QNamed Clause]) Source #
type AbsOfRef (QNamed Clause) Source #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract type AbsOfRef (QNamed Clause) = Clause
type AbsOfRef (List1 (QNamed Clause)) Source #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract type AbsOfRef (List1 (QNamed Clause)) = List1 Clause
type AbsOfRef [QNamed Clause] Source #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract type AbsOfRef [QNamed Clause] = [Clause]

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 #