Agda.Syntax.Reflected

Documentation

type Args = [Arg Term]

data Elim' a

Constructors

Apply (Arg a)

Instances

Unquote Elim

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM Elim

Show a => Show (Elim' a)

Defined in Agda.Syntax.Reflected

Methods

showsPrec :: Int -> Elim' a -> ShowS

show :: Elim' a -> String

showList :: [Elim' a] -> ShowS

ToAbstract (Expr, Elim)

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef (Expr, Elim)

Methods

toAbstract :: MonadReflectedToAbstract m => (Expr, Elim) -> m (AbsOfRef (Expr, Elim))

ToAbstract (Expr, Elims)

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef (Expr, Elims)

Methods

toAbstract :: MonadReflectedToAbstract m => (Expr, Elims) -> m (AbsOfRef (Expr, Elims))

type AbsOfRef (Expr, Elim)

Defined in Agda.Syntax.Translation.ReflectedToAbstract

type AbsOfRef (Expr, Elim) = Expr

type AbsOfRef (Expr, Elims)

Defined in Agda.Syntax.Translation.ReflectedToAbstract

type AbsOfRef (Expr, Elims) = Expr

type Elim = Elim' Term

type Elims = [Elim]

argsToElims :: Args -> Elims

data Abs a

Constructors

Abs String a

Instances

ToAbstract r => ToAbstract (Abs r)

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef (Abs r)

Methods

toAbstract :: MonadReflectedToAbstract m => Abs r -> m (AbsOfRef (Abs r))

Unquote a => Unquote (Abs a)

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM (Abs a)

Show a => Show (Abs a)

Defined in Agda.Syntax.Reflected

Methods

showsPrec :: Int -> Abs a -> ShowS

show :: Abs a -> String

showList :: [Abs a] -> ShowS

type AbsOfRef (Abs r)

Defined in Agda.Syntax.Translation.ReflectedToAbstract

type AbsOfRef (Abs r) = (AbsOfRef r, Name)

data Term

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

ToAbstract Term

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef Term

Methods

toAbstract :: MonadReflectedToAbstract m => Term -> m (AbsOfRef Term)

Unquote Elim

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM Elim

Unquote Term

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term0 -> UnquoteM Term

Show Term

Defined in Agda.Syntax.Reflected

Methods

showsPrec :: Int -> Term -> ShowS

show :: Term -> String

showList :: [Term] -> ShowS

ToAbstract (Expr, Elim)

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef (Expr, Elim)

Methods

toAbstract :: MonadReflectedToAbstract m => (Expr, Elim) -> m (AbsOfRef (Expr, Elim))

ToAbstract (Expr, Elims)

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef (Expr, Elims)

Methods

toAbstract :: MonadReflectedToAbstract m => (Expr, Elims) -> m (AbsOfRef (Expr, Elims))

type AbsOfRef Term

Defined in Agda.Syntax.Translation.ReflectedToAbstract

type AbsOfRef Term = Expr

type AbsOfRef (Expr, Elim)

Defined in Agda.Syntax.Translation.ReflectedToAbstract

type AbsOfRef (Expr, Elim) = Expr

type AbsOfRef (Expr, Elims)

Defined in Agda.Syntax.Translation.ReflectedToAbstract

type AbsOfRef (Expr, Elims) = Expr

type Type = Term

data Sort

Constructors

SetS Term

LitS Integer

PropS Term

PropLitS Integer

InfS Integer

UnknownS

Instances

ToAbstract Sort

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef Sort

Methods

toAbstract :: MonadReflectedToAbstract m => Sort -> m (AbsOfRef Sort)

Unquote Sort

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM Sort

Show Sort

Defined in Agda.Syntax.Reflected

Methods

showsPrec :: Int -> Sort -> ShowS

show :: Sort -> String

showList :: [Sort] -> ShowS

type AbsOfRef Sort

Defined in Agda.Syntax.Translation.ReflectedToAbstract

type AbsOfRef Sort = Expr

data Pattern

Constructors

ConP QName [Arg Pattern]

DotP Term

VarP Int

LitP Literal

AbsurdP Int

ProjP QName

Instances

ToAbstract Pattern

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef Pattern

Methods

toAbstract :: MonadReflectedToAbstract m => Pattern -> m (AbsOfRef Pattern)

Unquote Pattern

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM Pattern

Show Pattern

Defined in Agda.Syntax.Reflected

Methods

showsPrec :: Int -> Pattern -> ShowS

show :: Pattern -> String

showList :: [Pattern] -> ShowS

type AbsOfRef Pattern

Defined in Agda.Syntax.Translation.ReflectedToAbstract

type AbsOfRef Pattern = Pattern

data Clause

Constructors

Clause

Fields

• clauseTel :: [(Text, Arg Type)]
• clausePats :: [Arg Pattern]
• clauseRHS :: Term

AbsurdClause

Fields

• clauseTel :: [(Text, Arg Type)]
• clausePats :: [Arg Pattern]

Instances

Unquote Clause

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM Clause

Show Clause

Defined in Agda.Syntax.Reflected

Methods

showsPrec :: Int -> Clause -> ShowS

show :: Clause -> String

showList :: [Clause] -> ShowS

ToAbstract (QNamed Clause)

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef (QNamed Clause)

Methods

toAbstract :: MonadReflectedToAbstract m => QNamed Clause -> m (AbsOfRef (QNamed Clause))

ToAbstract (List1 (QNamed Clause))

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef (List1 (QNamed Clause))

Methods

toAbstract :: MonadReflectedToAbstract m => List1 (QNamed Clause) -> m (AbsOfRef (List1 (QNamed Clause)))

ToAbstract [QNamed Clause]

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Associated Types

type AbsOfRef [QNamed Clause]

Methods

toAbstract :: MonadReflectedToAbstract m => [QNamed Clause] -> m (AbsOfRef [QNamed Clause])

type AbsOfRef (QNamed Clause)

Defined in Agda.Syntax.Translation.ReflectedToAbstract

type AbsOfRef (QNamed Clause) = Clause

type AbsOfRef (List1 (QNamed Clause))

Defined in Agda.Syntax.Translation.ReflectedToAbstract

type AbsOfRef (List1 (QNamed Clause)) = List1 Clause

type AbsOfRef [QNamed Clause]

Defined in Agda.Syntax.Translation.ReflectedToAbstract

type AbsOfRef [QNamed Clause] = [Clause]

data Definition

Constructors

FunDef Type [Clause]

DataDef

RecordDef

DataConstructor

Axiom

Primitive

Instances

Show Definition

Defined in Agda.Syntax.Reflected

Methods

showsPrec :: Int -> Definition -> ShowS

show :: Definition -> String

showList :: [Definition] -> ShowS