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?

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.

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.

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.

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

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

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

Returns the list of elements in the discrimination tree.

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.

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

Render the list of simp lemmas.

def Batteries.Tactic.Lint.simpNF : Linter

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

def Batteries.Tactic.Lint.simpVarHead : Linter

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

def Batteries.Tactic.Lint.simpComm : Linter

A linter for commutativity lemmas that are marked simp.