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))
costIotaStep :: Int
costIncrease :: Int
costAppVar :: Int
costAppHint :: Int
costLamUnfold :: Int
costAbsurdLam :: Int
costEqStep :: Int
costEqCong :: Int
prioNoIota :: Int
prioCompCopy :: Int
prioCompUnif :: Int
prioCompIota :: Int
prioCompBeta :: Int
prioTypecheck :: Num a => Bool -> a
prioProjIndex :: Int