Agda-2.2.10: A dependently typed functional programming language and proof assistantSource codeContentsIndex
Agda.Auto.Syntax
Documentation
type UId o = Metavar (Exp o) (RefInfo o)Source
data HintMode Source
Constructors
HMNormal
HMRecCall
data EqReasoningConsts o Source
Constructors
EqReasoningConsts
eqrcId :: ConstRef o
eqrcBegin :: ConstRef o
eqrcStep :: ConstRef o
eqrcEnd :: ConstRef o
eqrcSym :: ConstRef o
eqrcCong :: ConstRef o
data EqReasoningState Source
Constructors
EqRSNone
EqRSChain
EqRSPrf1
EqRSPrf2
EqRSPrf3
data RefInfo o Source
Constructors
RIEnv
rieHints :: [(ConstRef o, HintMode)]
rieDefFreeVars :: Nat
rieEqReasoningConsts :: Maybe (EqReasoningConsts o)
RIMainInfo Nat (HNExp o) Bool
forall a . RIUnifInfo [CAction o] (HNExp o)
RICopyInfo (ICExp o)
RIIotaStep Bool
RIInferredTypeUnknown
RINotConstructor
RIUsedVars [UId o] [Elr o]
RIPickSubsvar
RIEqRState EqReasoningState
RICheckElim Bool
RICheckProjIndex [ConstRef 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
cddeffreevars :: Nat
data DeclCont o Source
Constructors
Def Nat [Clause o] (Maybe Nat) (Maybe Nat)
Datatype [ConstRef o] [ConstRef o]
Constructor Nat
Postulate
type Clause o = ([Pat o], MExp o)Source
data Pat o Source
Constructors
PatConApp (ConstRef o) [Pat o]
PatVar String
PatExp
type ConstRef o = IORef (ConstDef o)Source
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
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)
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
data HNArgList o Source
Constructors
HNALNil
HNALCons FMode (ICExp o) (ICArgList o)
HNALConPar (ICArgList o)
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
data TrBr a o Source
Constructors
TrBr [MExp o] a
data CAction o Source
Constructors
Sub (ICExp o)
Skip
Weak Nat
type Ctx o = [(MId, CExp o)]Source
type EE = IOSource
detecteliminand :: [Clause o] -> Maybe NatSource
detectsemiflex :: ConstRef o -> [Clause o] -> IO BoolSource
categorizedecl :: ConstRef o -> IO ()Source
metaliseokh :: MExp o -> IO (MExp o)Source
expandExp :: MExp o -> IO (MExp o)Source
addtrailingargs :: Clos (MArgList o) o -> ICArgList o -> ICArgList oSource
closify :: MExp o -> CExp oSource
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
weakarglist :: Nat -> ICArgList o -> ICArgList oSource
weakelr :: Nat -> Elr o -> Elr oSource
doclos :: [CAction o] -> Nat -> Either Nat (ICExp o)Source
Produced by Haddock version 2.6.1