Candidates

inductive GeneralizationLinter.WeakeningShape : Type

The kinds of possible weakening suggestions.

• drop : WeakeningShape

  Binder may be droppable: as far as the linter can tell, nothing requires it, or everything it would have to provide is already available without it.

• weaken (weakerVertex : Vertex) : WeakeningShape

  Binder may be weakenable to weakerVertex.

• split (weakerVertices : Array Vertex) : WeakeningShape

  Binder may be weakenable by splitting it up into weakerVertices.

@[implicit_reducible]

instance GeneralizationLinter.instInhabitedWeakeningShape : Inhabited WeakeningShape

Equations

• GeneralizationLinter.instInhabitedWeakeningShape = { default := GeneralizationLinter.instInhabitedWeakeningShape.default }

structure GeneralizationLinter.Candidate : Type

An unverified weakening candidate.

• binder : TargetedBinder

  The binder this candidate proposes weakening.

• shape : WeakeningShape

  The kind of weakening this candidate proposes.

@[implicit_reducible]

instance GeneralizationLinter.instInhabitedCandidate : Inhabited Candidate

Equations

• GeneralizationLinter.instInhabitedCandidate = { default := GeneralizationLinter.instInhabitedCandidate.default }

def GeneralizationLinter.Candidate.replacements (c : Candidate) : Array Vertex

The Vertexes of the classes of the proposed replacements.

Equations

• One or more equations did not get rendered due to their size.

def GeneralizationLinter.Vertex.unifiable (u v : Vertex) : Bool

Returns true iff u and v can be unified.

Note: We use syntactic equality in this process, so e.g. OrderDual ℕ does not unify with ℕ according to us, even though Lean's actual unification mechanism would unify them, since it uses definitional equality.

---

Examples

Vertex.unifiable (Monoid #0) (Semigroup #0) = false
Vertex.unifiable (Pow #0 ℕ) (Pow #0 ℤ) = false
Vertex.unifiable (Pow #0 ℕ) (Pow #0 #1) = true
Vertex.unifiable (Module #0 #0) (Module #0 #1) = true
Vertex.unifiable (Module #0 #0) (Module #0 (MulOpposite #0)) = false

Equations

• One or more equations did not get rendered due to their size.

def GeneralizationLinter.mcaCandidates (graph : ClassGraph) (binders : Array TargetedBinder) (reqs : Array Requirement) (cfg : LinterConfig := { }) (includeSubsumers : Bool := true) : Array Candidate

Return a (possibly empty) array of candidate weakenings for any of the targeted binders binders such that the requirements reqs are still satisfied.

Equations

• One or more equations did not get rendered due to their size.