Agda-2.2.6: A dependently typed functional programming language and proof assistantSource codeContentsIndex
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)
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
data MId Source
Constructors
Id String
NoId
data Abs a Source
Constructors
Abs MId a
data ConstDef o Source
Constructors
ConstDef
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
type MExp o = MM (Exp o) (RefInfo o)Source
data ArgList o Source
Constructors
ALNil
ALCons FMode (MExp o) (MArgList o)
ALConPar (MArgList o)
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
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)
data Clos a o Source
Constructors
Clos [CAction o] a
data CAction o Source
Constructors
Sub (CExp o)
Skip
Weak Nat
type Ctx o = [(MId, CExp o)]Source
type EE = IOSource
data Elrs o Source
Constructors
ElrsNil
ElrsCons (Elr o) (Elrs o)
ElrsWeak (Elrs o)
Produced by Haddock version 2.6.0