structure GeneralizationLinter.PinnedBinder : Type

• pos : Nat
• name : Lean.Name
• level : Nat

@[implicit_reducible]

instance GeneralizationLinter.instInhabitedPinnedBinder : Inhabited PinnedBinder

Equations

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

def GeneralizationLinter.pinnedTypeBinders (type : Lean.Expr) : Lean.MetaM (Array PinnedBinder)

Equations

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

structure GeneralizationLinter.UniverseGeneralizations : Type

• blocks : Array (Array PinnedBinder)
• statement : Lean.Expr
• params : Array Lean.Name

@[implicit_reducible]

instance GeneralizationLinter.instInhabitedUniverseGeneralizations : Inhabited UniverseGeneralizations

Equations

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

def GeneralizationLinter.universeGeneralizationsBlocks? (const : Lean.ConstantInfo) (declSig bodyStx : Lean.Syntax) (blocks : Array (Array PinnedBinder)) (wrappers : Array Lean.Syntax := #[]) : Lean.Elab.TermElabM (Option UniverseGeneralizations)

Equations

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

def GeneralizationLinter.universeGeneralizations? (const : Lean.ConstantInfo) (declSig bodyStx : Lean.Syntax) (bs : Array PinnedBinder) (wrappers : Array Lean.Syntax := #[]) : Lean.Elab.TermElabM (Option UniverseGeneralizations)

Equations

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

def GeneralizationLinter.universeGeneralization? (const : Lean.ConstantInfo) (declSig bodyStx : Lean.Syntax) (b : PinnedBinder) (wrappers : Array Lean.Syntax := #[]) : Lean.Elab.TermElabM (Option UniverseGeneralizations)

Equations

• GeneralizationLinter.universeGeneralization? const declSig bodyStx b wrappers = GeneralizationLinter.universeGeneralizations? const declSig bodyStx #[b] wrappers

def GeneralizationLinter.sharedSubsetLadder? {α : Type} (grp : Array PinnedBinder) (gate : Array PinnedBinder → Lean.Elab.TermElabM (Option α)) : Lean.Elab.TermElabM (Option (Array PinnedBinder × α))

Equations

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