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, Elims) Expr

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Methods

toAbstract :: (Expr, Elims) -> WithNames Expr

ToAbstract (Expr, Elim) Expr

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Methods

toAbstract :: (Expr, Elim) -> WithNames Expr

type Elim = Elim' Term

type Elims = [Elim]

argsToElims :: Args -> Elims

data Abs a

Constructors

Abs String a

Instances

Show a => Show (Abs a)

Defined in Agda.Syntax.Reflected

Methods

showsPrec :: Int -> Abs a -> ShowS

show :: Abs a -> String

showList :: [Abs a] -> ShowS

Unquote a => Unquote (Abs a)

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM (Abs a)

ToAbstract r a => ToAbstract (Abs r) (a, Name)

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Methods

toAbstract :: Abs r -> WithNames (a, Name)

data Term

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

Defined in Agda.Syntax.Reflected

Methods

showsPrec :: Int -> Term -> ShowS

show :: Term -> String

showList :: [Term] -> ShowS

PrettyTCM Term

Defined in Agda.TypeChecking.Pretty

Methods

prettyTCM :: Term -> TCM Doc

Unquote Term

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term0 -> UnquoteM Term

Unquote Elim

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM Elim

ToAbstract Term Expr

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Methods

toAbstract :: Term -> WithNames Expr

ToAbstract [Arg Term] [NamedArg Expr]

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Methods

toAbstract :: [Arg Term] -> WithNames [NamedArg Expr]

ToAbstract (Expr, Elims) Expr

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Methods

toAbstract :: (Expr, Elims) -> WithNames Expr

ToAbstract (Expr, Elim) Expr

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Methods

toAbstract :: (Expr, Elim) -> WithNames Expr

type Type = Term

data Sort

Constructors

SetS Term

LitS Integer

UnknownS

Instances

Show Sort

Defined in Agda.Syntax.Reflected

Methods

showsPrec :: Int -> Sort -> ShowS

show :: Sort -> String

showList :: [Sort] -> ShowS

Unquote Sort

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM Sort

ToAbstract Sort Expr

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Methods

toAbstract :: Sort -> WithNames Expr

data Pattern

Constructors

ConP QName [Arg Pattern]

DotP

VarP String

LitP Literal

AbsurdP

ProjP QName

Instances

Show Pattern

Defined in Agda.Syntax.Reflected

Methods

showsPrec :: Int -> Pattern -> ShowS

show :: Pattern -> String

showList :: [Pattern] -> ShowS

Unquote Pattern

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM Pattern

ToAbstract Pattern (Names, Pattern)

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Methods

toAbstract :: Pattern0 -> WithNames (Names, Pattern)

data Clause

Constructors

Clause [Arg Pattern] Term

AbsurdClause [Arg Pattern]

Instances

Show Clause

Defined in Agda.Syntax.Reflected

Methods

showsPrec :: Int -> Clause -> ShowS

show :: Clause -> String

showList :: [Clause] -> ShowS

Unquote Clause

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM Clause

ToAbstract (QNamed Clause) Clause

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Methods

toAbstract :: QNamed Clause0 -> WithNames Clause

ToAbstract [QNamed Clause] [Clause]

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Methods

toAbstract :: [QNamed Clause0] -> WithNames [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