Agda-2.5.1: A dependently typed functional programming language and proof assistant

Safe HaskellNone
LanguageHaskell98

Agda.Syntax.Reflected

Documentation

type Args = [Arg Term] Source

data Elim' a Source

Constructors

Apply (Arg a) 

Instances

Unquote Elim Source 
Show a => Show (Elim' a) Source 
ToAbstract (Expr, Elims) Expr Source 
ToAbstract (Expr, Elim) Expr Source 

type Elim = Elim' Term Source

type Elims = [Elim] Source

argsToElims :: Args -> Elims Source

data Abs a Source

Constructors

Abs String a 

Instances

Show a => Show (Abs a) Source 
Unquote a => Unquote (Abs a) Source 
ToAbstract r a => ToAbstract (Abs r) (a, Name) Source 

data Term Source

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

type Type = Term Source

data Sort Source

Constructors

SetS Term 
LitS Integer 
UnknownS 

Instances

data Pattern Source

Constructors

ConP QName [Arg Pattern] 
DotP 
VarP String 
LitP Literal 
AbsurdP 
ProjP QName 

Instances

data Clause Source

Constructors

Clause [Arg Pattern] Term 
AbsurdClause [Arg Pattern] 

Instances

data Definition Source

Constructors

FunDef Type [Clause] 
DataDef 
RecordDef 
DataConstructor 
Axiom 
Primitive 

Instances