inductive GeneralizationLinter.WeakeningShape : Type

The kinds of possible weakening suggestions.

• drop : WeakeningShape

  Binder is entirely unused, and can therefore be dropped (removed).

• weaken (target : Vertex) : WeakeningShape

  Binder can be weakened to target.

• split (targets : Array Vertex) : WeakeningShape

  Binder can be weakened by splitting it up into targets.

@[implicit_reducible]

instance GeneralizationLinter.instInhabitedWeakeningShape : Inhabited WeakeningShape

Equations

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

structure GeneralizationLinter.Candidate : Type

An unverified weakening proposal. See also ConfirmedWeakening.

• 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.Candidate.replacementNames (c : Candidate) : Array Lean.Name

The Names of the classes of the proposed replacements.

Equations

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

def GeneralizationLinter.Candidate.singleWeakening? (c : Candidate) : Option Vertex

If c is a weakening candidate proposing to weaken a binder to a specific target t, return some t. If c proposes dropping the binder or splitting it, return none.

Equations

• c.singleWeakening? = match c.shape with | GeneralizationLinter.WeakeningShape.weaken t => some t | x => none

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.

Equations

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

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

#TODO

Equations

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