Agda-2.3.0: A dependently typed functional programming language and proof assistant
Agda.Auto.SearchControl
data ExpRefInfo o Source
Constructors
Fields
univar :: [CAction o] -> Nat -> Maybe NatSource
subsvars :: [CAction o] -> [Nat]Source
costIotaStep, costIncrease, costAppExtraRef :: IntSource
prioNo, prioAbsurdLambda, prioNoIota, prioCompCopy, prioCompUnif, prioCompChoice, prioCompIota, prioCompareArgList, prioCompBetaStructured, prioCompBeta, prioInferredTypeUnknown, prioTypecheckArgList, prioTypeUnknown :: IntSource