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) 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 #
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 #
type AbsOfRef (Expr, Elims) Source #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract type AbsOfRef (Expr, Elims) = Expr
type AbsOfRef (Expr, Elim) Source #
Instance details Defined in Agda.Syntax.Translation.ReflectedToAbstract type AbsOfRef (Expr, Elim) = 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

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 #
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 #
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

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

type Type = Term Source #

data Sort Source #

Constructors

SetS Term
LitS Integer
PropS Term
PropLitS Integer
InfS 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 #
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 #
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

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

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] 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 #