Agda-2.6.20240714: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

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) 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

type AbsOfRef (Expr, Elim) = Expr

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) 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

type AbsOfRef (Expr, Elims) = Expr

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) 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

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

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 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

type AbsOfRef Term = Expr

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 :: Term -> 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) 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

type AbsOfRef (Expr, Elim) = Expr

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) 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

type AbsOfRef (Expr, Elims) = Expr

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 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

type AbsOfRef Sort = Expr

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 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

type AbsOfRef Pattern = Pattern

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

AbsurdClause 

Fields

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) 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

type AbsOfRef (QNamed Clause) = Clause

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)) 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

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

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] 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

type AbsOfRef [QNamed Clause] = [Clause]

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