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

getinfo :: [RefInfo o] -> ExpRefInfo o

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

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

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

costIotaStep :: Int

costIncrease :: Int

costAppExtraRef :: Int

costUnificationOccurs :: Int

costUnification :: Int

costAppVar :: Int

costAppVarUsed :: Int

costAppHint :: Int

costAppHintUsed :: Int

costAppRecCall :: Int

costAppRecCallUsed :: Int

costAppConstructor :: Int

costAppConstructorSingle :: Int

costLam :: Int

costLamUnfold :: Int

costPi :: Int

costSort :: Int

costInferredTypeUnkown :: Int

costAbsurdLam :: Int

costEqStep :: Int

costEqEnd :: Int

costEqSym :: Int

costEqCong :: Int

prioNo :: Int

prioAbsurdLambda :: Int

prioNoIota :: Int

prioCompCopy :: Int

prioCompUnif :: Int

prioCompChoice :: Int

prioCompIota :: Int

prioCompareArgList :: Int

prioCompBetaStructured :: Int

prioCompBeta :: Int

prioInferredTypeUnknown :: Int

prioTypecheckArgList :: Int

prioTypeUnknown :: Int

prioTypecheck :: Num a => Bool -> a

prioProjIndex :: Int