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

Agda.Auto.Syntax

Documentation

type UId o = Metavar (Exp o) (RefInfo o)Source

data HintMode Source

Constructors

HMNormal 
HMRecCall 

type MyPB o = PB (RefInfo o)Source

type MyMB a o = MB a (RefInfo o)Source

type Nat = IntSource

data FMode Source

Constructors

Hidden 
Instance 
NotHidden 

Instances

data MId Source

Constructors

Id String 
NoId 

Instances

Trav (MId, CExp o) (RefInfo o) 

data Abs a Source

Constructors

Abs MId a 

data ConstDef o Source

Constructors

ConstDef 

Fields

cdname :: String
 
cdorigin :: o
 
cdtype :: MExp o
 
cdcont :: DeclCont o
 
cddeffreevars :: Nat
 

Instances

type Clause o = ([Pat o], MExp o)Source

data Pat o Source

Constructors

PatConApp (ConstRef o) [Pat o] 
PatVar String 
PatExp 

data Elr o Source

Constructors

Var Nat 
Const (ConstRef o) 

data Sort Source

Constructors

Set Nat 
UnknownSort 
Type 

data Exp o Source

Constructors

App (Maybe (UId o)) (OKHandle (RefInfo o)) (Elr o) (MArgList o) 
Lam FMode (Abs (MExp o)) 
Pi (Maybe (UId o)) FMode Bool (MExp o) (Abs (MExp o)) 
Sort Sort 
AbsurdLambda FMode 

Instances

Refinable (ICExp o) (RefInfo o) 
Refinable (Exp o) (RefInfo o) 
Trav (Exp o) (RefInfo o) 
Trav (MId, CExp o) (RefInfo o) 

type MExp o = MM (Exp o) (RefInfo o)Source

data ArgList o Source

Constructors

ALNil 
ALCons FMode (MExp o) (MArgList o) 
ALProj (MArgList o) (MM (ConstRef o) (RefInfo o)) FMode (MArgList o) 
ALConPar (MArgList o) 

Instances

type MArgList o = MM (ArgList o) (RefInfo o)Source

data HNExp o Source

Constructors

HNApp [Maybe (UId o)] (Elr o) (ICArgList o) 
HNLam [Maybe (UId o)] FMode (Abs (ICExp o)) 
HNPi [Maybe (UId o)] FMode Bool (ICExp o) (Abs (ICExp o)) 
HNSort Sort 

type ICExp o = Clos (MExp o) oSource

type CExp o = TrBr (ICExp o) oSource

data ICArgList o Source

Constructors

CALNil 
CALConcat (Clos (MArgList o) o) (ICArgList o) 

data Clos a o Source

Constructors

Clos [CAction o] a 

Instances

Refinable (ICExp o) (RefInfo o) 
Trav (MId, CExp o) (RefInfo o) 

data TrBr a o Source

Constructors

TrBr [MExp o] a 

Instances

Trav (MId, CExp o) (RefInfo o) 
Trav (TrBr a o) (RefInfo o) 

data CAction o Source

Constructors

Sub (ICExp o) 
Skip 
Weak Nat 

type Ctx o = [(MId, CExp o)]Source

type EE = IOSource

sub :: MExp o -> CExp o -> CExp oSource

subi :: MExp o -> ICExp o -> ICExp oSource

weak :: Nat -> CExp o -> CExp oSource

weaki :: Nat -> Clos a o -> Clos a oSource

weakelr :: Nat -> Elr o -> Elr oSource