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

Agda.Auto.SearchControl

# Documentation

data ExpRefInfo o

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

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

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

costAppExtraRef :: Int

costIncrease :: Int

costIotaStep :: Int

prioTypeUnknown :: Int

prioTypecheckArgList :: Int

prioInferredTypeUnknown :: Int

prioCompBeta :: Int

prioCompBetaStructured :: Int

prioCompareArgList :: Int

prioCompIota :: Int

prioCompChoice :: Int

prioCompUnif :: Int

prioCompCopy :: Int

prioNoIota :: Int

prioAbsurdLambda :: Int

prioNo :: Int