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

Safe HaskellSafe-Infered

Agda.Auto.Syntax

Documentation

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

data HintMode

Constructors

HMNormal 
HMRecCall 

type MyPB o = PB (RefInfo o)

type MyMB a o = MB a (RefInfo o)

type Nat = Int

data FMode

Constructors

Hidden 
Instance 
NotHidden 

Instances

data MId

Constructors

Id String 
NoId 

Instances

Trav (MId, CExp o) (RefInfo o) 

data Abs a

Constructors

Abs MId a 

data ConstDef o

Constructors

ConstDef 

Fields

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

Instances

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

data Pat o

Constructors

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

type ConstRef o = IORef (ConstDef o)

data Elr o

Constructors

Var Nat 
Const (ConstRef o) 

data Sort

Constructors

Set Nat 
UnknownSort 
Type 

data Exp o

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)

data ArgList o

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)

data HNExp o

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 

data HNArgList o

type ICExp o = Clos (MExp o) o

type CExp o = TrBr (ICExp o) o

data ICArgList o

Constructors

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

data Clos a o

Constructors

Clos [CAction o] a 

Instances

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

data TrBr a o

Constructors

TrBr [MExp o] a 

Instances

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

data CAction o

Constructors

Sub (ICExp o) 
Skip 
Weak Nat 

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

type EE = IO

metaliseokh :: MExp o -> IO (MExp o)

expandExp :: MExp o -> IO (MExp o)

closify :: MExp o -> CExp o

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

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

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

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

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

doclos :: [CAction o] -> Nat -> Either Nat (ICExp o)