Something went wrong. Try again.
The Package Calculus
Something went wrong. Try again.
543 B · 16 lines
at dev
1234567891011121314151617import PackageCalculus.Versions.Formula
/-! # Reducing version-formula resolutions to base resolutions
`vfReduce` evaluates every `VersionFormula` in a `VFDepRel` against theavailable versions in `R`, producing a plain `DepRel`. -/
namespace PackageCalculus
variable {N : Type*} [DecidableEq N] {V : Type*} [LT V] [DecidableEq V] [DecidableRel (· < · : V → V → Prop)]
def vfReduce (R : Real N V) (Δ_Φ : VFDepRel N V) : DepRel N V := Δ_Φ.image (fun ⟨p, m, φ⟩ => (p, m, φ.eval (repoVersions R m)))
end PackageCalculus