Linter for simplification lemmas

This files defines several linters that prevent common mistakes when declaring simp lemmas:

• simpNF checks that the left-hand side of a simp lemma is not simplified by a different lemma.
• simpVarHead checks that the head symbol of the left-hand side is not a variable.
• simpComm checks that commutativity lemmas are not marked as simplification lemmas.

structure Batteries.Tactic.Lint.SimpTheoremInfo : Type

The data associated to a simp theorem.

• hyps : Array Lean.Expr

  The hypotheses of the theorem

• isConditional : Bool

  True if this is a conditional rewrite rule

• lhs : Lean.Expr

  The thing to replace

• rhs : Lean.Expr

  The result of replacement

def Batteries.Tactic.Lint.isConditionalHyps (lhs : Lean.Expr) : List Lean.Expr → Lean.MetaM Bool

Given the list of hypotheses, is this a conditional rewrite rule?

Equations

• One or more equations did not get rendered due to their size.
• Batteries.Tactic.Lint.isConditionalHyps lhs [] = pure false

def Batteries.Tactic.Lint.withSimpTheoremInfos {α : Type} (ty : Lean.Expr) (k : SimpTheoremInfo → Lean.MetaM α) : Lean.MetaM (Array α)

Runs the continuation on all the simp theorems encoded in the given type.

Equations

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

def Batteries.Tactic.Lint.isSimpEq (a b : Lean.Expr) (whnfFirst : Bool := true) : Lean.MetaM Bool

Checks whether two expressions are equal for the simplifier. That is, they are reducibly-definitional equal, and they have the same head symbol.

Equations

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

def Batteries.Tactic.Lint.checkAllSimpTheoremInfos (ty : Lean.Expr) (k : SimpTheoremInfo → Lean.MetaM (Option Lean.MessageData)) : Lean.MetaM (Option Lean.MessageData)

Constructs a message from all the simp theorems encoded in the given type.

Equations

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

def Batteries.Tactic.Lint.isSimpTheorem (declName : Lean.Name) : Lean.MetaM Bool

Returns true if this is a @[simp] declaration.

Equations

• Batteries.Tactic.Lint.isSimpTheorem declName = do let __do_lift ← liftM Lean.Meta.getSimpTheorems pure (Lean.PersistentHashSet.contains __do_lift.lemmaNames (Lean.Meta.Origin.decl declName))

def Lean.Meta.DiscrTree.elements {α : Type} (d : DiscrTree α) : Array α

Returns the list of elements in the discrimination tree.

Equations

• d.elements = d.root.foldl (fun (arr : Array α) (x : Lean.Meta.DiscrTree.Key) => Lean.Meta.DiscrTree.elements.trieElements arr) #[]

partial def Lean.Meta.DiscrTree.elements.trieElements {α : Type} (arr : Array α) : Trie α → Array α

Returns the list of elements in the trie.

def Batteries.Tactic.Lint.decorateError {α : Type} (msg : Lean.MessageData) (k : Lean.MetaM α) : Lean.MetaM α

Add message msg to any errors thrown inside k.

Equations

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

def Batteries.Tactic.Lint.formatLemmas (usedSimps : Lean.Meta.Simp.UsedSimps) (simpName : String) : Lean.MetaM Lean.MessageData

Render the list of simp lemmas.

Equations

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

def Batteries.Tactic.Lint.simpNF : Linter

A linter for simp lemmas whose lhs is not in simp-normal form, and which hence never fire.

Equations

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

def Batteries.Tactic.Lint.simpVarHead : Linter

A linter for simp lemmas whose lhs has a variable as head symbol, and which hence never fire.

Equations

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

def Batteries.Tactic.Lint.simpComm : Linter

A linter for commutativity lemmas that are marked simp.

Equations

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