Safe Haskell | Safe-Infered |
---|
Agda.Auto.SearchControl
Documentation
data ExpRefInfo o
Constructors
ExpRefInfo | |
Fields
|
getinfo :: [RefInfo o] -> ExpRefInfo o
extraref :: UId o -> [Maybe (UId o)] -> ConstRef o -> (Int, StateT (IORef [SubConstraints (RefInfo o)], Int) IO (Exp o))
costAppVar :: Int
costAppHint :: Int
costLamUnfold :: Int
costAbsurdLam :: Int
costEqStep :: Int
costEqCong :: Int
prioNo, prioAbsurdLambda, prioNoIota, prioCompCopy, prioCompUnif, prioCompChoice, prioCompIota, prioCompareArgList, prioCompBetaStructured, prioCompBeta, prioInferredTypeUnknown, prioTypecheckArgList, prioTypeUnknown :: Int
prioTypecheck :: Num a => Bool -> a
prioProjIndex :: Int