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.

structure Std.Tactic.Lint.SimpTheoremInfo :

The hypotheses of the theorem
hyps : Array Lean.Expr
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

def Std.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.
Std.Tactic.Lint.isConditionalHyps lhs [] = pure false

def Std.Tactic.Lint.withSimpTheoremInfos {α : Type} (ty : Lean.Expr) (k : Std.Tactic.Lint.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 Std.Tactic.Lint.isSimpEq (a : Lean.Expr) (b : Lean.Expr) (whnfFirst : optParam 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 Std.Tactic.Lint.checkAllSimpTheoremInfos (ty : Lean.Expr) (k : Std.Tactic.Lint.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 Std.Tactic.Lint.isSimpTheorem (declName : Lean.Name) :

Lean.MetaM Bool

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

Equations

Std.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} {s : Bool} (d : Lean.Meta.DiscrTree α s) :

Returns the list of elements in the discrimination tree.

Equations

Lean.Meta.DiscrTree.elements d = Lean.PersistentHashMap.foldl d.root (fun arr x => Lean.Meta.DiscrTree.elements.trieElements arr) #[]

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

Lean.Meta.DiscrTree.Trie α s → Array α

Returns the list of elements in the trie.

def Std.Tactic.Lint.decorateError {α : Type} (msg : Lean.MessageData) (k : 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 Std.Tactic.Lint.formatLemmas (usedSimps : Lean.Meta.Simp.UsedSimps) :

Lean.MetaM Lean.MessageData

Render the list of simp lemmas.

Equations

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

def Std.Tactic.Lint.simpNF :

Std.Tactic.Lint.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 Std.Tactic.Lint.simpVarHead :

Std.Tactic.Lint.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 Std.Tactic.Lint.simpComm :

Std.Tactic.Lint.Linter

A linter for commutativity lemmas that are marked simp.

Equations

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