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