Agda-2.2.6: A dependently typed functional programming language and proof assistant
Agda.Auto.Syntax
data RefInfo o Source
Constructors
Instances
type MyPB o = PB (RefInfo o)Source
type MyMB a o = MB a (RefInfo o)Source
type Nat = IntSource
data FMode Source
data MId Source
data Abs a Source
data ConstDef o Source
Fields
data DeclCont o Source
type Clause o = ([Pat o], MExp o)Source
data Pat o Source
type ConstRef o = IORef (ConstDef o)Source
data Elr o Source
data Sort Source
data Exp o Source
type MExp o = MM (Exp o) (RefInfo o)Source
data ArgList o Source
type MArgList o = MM (ArgList o) (RefInfo o)Source
data HNExp o Source
data HNArgList o Source
type CExp o = Clos (MExp o) oSource
data CArgList o Source
data Clos a o Source
data CAction o Source
type Ctx o = [(MId, CExp o)]Source
type EE = IOSource
data Elrs o Source