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

Agda.Auto.Syntax

Documentation

data RefInfo o Source

Constructors

RIEnv [ConstRef o] 
RIMainInfo Nat (HNExp o) 
forall a . RIUnifInfo (Metavar a (RefInfo o)) [CAction o] (HNExp o) 

Instances

Refinable (ArgList o) (RefInfo o) 
Refinable (Exp o) (RefInfo o) 
Trav (CAction o) (RefInfo o) 
Trav (CArgList o) (RefInfo o) 
Trav (HNExp o) (RefInfo o) 
Trav (ArgList o) (RefInfo o) 
Trav (Exp o) (RefInfo o) 
Trav (MId, CExp o) (RefInfo o) 
Trav a (RefInfo o) => Trav (Clos a o) (RefInfo o) 

type MyPB o = PB (RefInfo o)Source

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

type Nat = IntSource

data FMode Source

Constructors

Hidden 
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
 

data DeclCont o Source

Constructors

Def Nat [Clause o] 
Datatype [ConstRef o] 
Constructor 
Postulate 

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

data Pat o Source

Constructors

PatConApp (ConstRef o) [Pat o] 
PatVar 
PatExp 

type ConstRef o = IORef (ConstDef o)Source

data Elr o Source

Constructors

Var Nat 
Const (ConstRef o) 

data Sort Source

Constructors

SortLevel Nat 
Type 

data Exp o Source

Constructors

App (Elr o) (MArgList o) 
Lam FMode (Abs (MExp o)) 
Fun FMode (MExp o) (MExp o) 
Pi FMode Bool (MExp o) (Abs (MExp o)) 
Sort Sort 

Instances

Refinable (Exp o) (RefInfo o) 
Trav (Exp o) (RefInfo o) 

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

data ArgList o Source

Constructors

ALNil 
ALCons FMode (MExp o) (MArgList o) 
ALConPar (MArgList o) 

Instances

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

data HNExp o Source

Constructors

HNApp (Elr o) (CArgList o) 
HNLam (Abs (CExp o)) 
HNFun FMode (CExp o) (CExp o) 
HNPi FMode Bool (CExp o) (Abs (CExp o)) 
HNSort Sort 

Instances

Trav (HNExp o) (RefInfo o) 

data HNArgList o Source

Constructors

HNALNil 
HNALCons (CExp o) (CArgList o) 
HNALConPar (CArgList o) 

type CExp o = Clos (MExp o) oSource

data CArgList o Source

Constructors

CALNil 
CALConcat (Clos (MArgList o) o) (CArgList o) 

Instances

data Clos a o Source

Constructors

Clos [CAction o] a 

Instances

Trav a (RefInfo o) => Trav (Clos a o) (RefInfo o) 

data CAction o Source

Constructors

Sub (CExp o) 
Skip 
Weak Nat 

Instances

Trav (CAction o) (RefInfo o) 

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

type EE = IOSource

data Elrs o Source

Constructors

ElrsNil 
ElrsCons (Elr o) (Elrs o) 
ElrsWeak (Elrs o)