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

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

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, Elim) Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

type AbsOfRef (Expr, Elims) Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

type Elims = [Elim] 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)
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 #

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

Unquote Elim Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

Unquote Term Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

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

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 Term Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

type AbsOfRef (Expr, Elim) Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

type AbsOfRef (Expr, Elims) Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

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

Unquote Sort Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

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

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

Unquote Pattern Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

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

data Clause Source #

Constructors

Clause 

Fields

AbsurdClause 

Fields

Instances

Instances details
Unquote Clause Source # 
Instance details

Defined in Agda.TypeChecking.Unquote

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

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

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

Defined in Agda.Syntax.Translation.ReflectedToAbstract

type AbsOfRef (List1 (QNamed Clause)) Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

type AbsOfRef [QNamed Clause] Source # 
Instance details

Defined in Agda.Syntax.Translation.ReflectedToAbstract

data Definition Source #

Instances

Instances details
Show Definition Source # 
Instance details

Defined in Agda.Syntax.Reflected

Methods

showsPrec :: Int -> Definition -> ShowS

show :: Definition -> String

showList :: [Definition] -> ShowS