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

Safe Haskell	Safe-Inferred

Agda.Auto.SearchControl

Documentation

data ExpRefInfo o Source

Constructors

ExpRefInfo
Fields eriMain :: Maybe (RefInfo o) eriUnifs :: [RefInfo o] eriInfTypeUnknown :: Bool eriIsEliminand :: Bool eriUsedVars :: Maybe ([UId o], [Elr o]) eriIotaStep :: Maybe Bool eriPickSubsVar :: Bool eriEqRState :: Maybe EqReasoningState

getinfo :: [RefInfo o] -> ExpRefInfo oSource

univar :: [CAction o] -> Nat -> Maybe Nat Source

subsvars :: [CAction o] -> [Nat]Source

extraref :: Metavar (Exp o) (RefInfo o) -> [Maybe (Metavar (Exp o) (RefInfo o))] -> ConstRef o -> (Int, StateT (IORef [SubConstraints (RefInfo o)], Int) IO (Exp o))Source

costIotaStep :: Int Source

costIncrease :: Int Source

costAppExtraRef :: Int Source

costUnificationOccurs :: Int Source

costUnification :: Int Source

costAppVar :: Int Source

costAppVarUsed :: Int Source

costAppHint :: Int Source

costAppHintUsed :: Int Source

costAppRecCall :: Int Source

costAppRecCallUsed :: Int Source

costAppConstructor :: Int Source

costAppConstructorSingle :: Int Source

costLam :: Int Source

costLamUnfold :: Int Source

costPi :: Int Source

costSort :: Int Source

costInferredTypeUnkown :: Int Source

costAbsurdLam :: Int Source

costEqStep :: Int Source

costEqEnd :: Int Source

costEqSym :: Int Source

costEqCong :: Int Source

prioNo :: Int Source

prioAbsurdLambda :: Int Source

prioNoIota :: Int Source

prioCompCopy :: Int Source

prioCompUnif :: Int Source

prioCompChoice :: Int Source

prioCompIota :: Int Source

prioCompareArgList :: Int Source

prioCompBetaStructured :: Int Source

prioCompBeta :: Int Source

prioInferredTypeUnknown :: Int Source

prioTypecheckArgList :: Int Source

prioTypeUnknown :: Int Source

prioTypecheck :: Num a => Bool -> aSource

prioProjIndex :: Int Source