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

Safe Haskell | Safe-Infered

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 :: UId o -> [Maybe (UId 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