# Documentation

Std.Tactic.Lint.Simp

# 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.
• The hypotheses of the theorem

hyps :
• True if this is a conditional rewrite rule

isConditional : Bool
• The thing to replace

lhs : Lean.Expr
• The result of replacement

rhs : Lean.Expr

The data associated to a simp theorem.

Instances For

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

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

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 Std.Tactic.Lint.isSimpEq (a : Lean.Expr) (b : Lean.Expr) (whnfFirst : ) :

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.

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.

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

Equations
def Lean.Meta.DiscrTree.elements {α : Type} {s : Bool} (d : ) :

Returns the list of elements in the discrimination tree.

Equations
partial def Lean.Meta.DiscrTree.elements.trieElements {α : Type} {s : Bool} (arr : ) :

Returns the list of elements in the trie.

Add message msg to any errors thrown inside k.

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

Render the list of simp lemmas.

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

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.

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.

A linter for commutativity lemmas that are marked simp.

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