Documentation Verification Report

Simp

📁 Source: Batteries/Tactic/Lint/Simp.lean

Statistics

Metric	Count
Definitions `SimpTheoremInfo`, `hyps`, `lhs`, `rhs`, `checkAllSimpTheoremInfos`, `decorateError`, `formatLemmas`, `isCondition`, `isSimpEq`, `isSimpTheorem`, `simpComm`, `simpNF`, `simpVarHead`, `withSimpTheoremInfos`, `elements`, `«simp-normal_form»`	16
Theorems	0
Total	16

Batteries.Tactic.Lint

Definitions

Name	Category	Theorems
`SimpTheoremInfo` 📖	CompData	—
`checkAllSimpTheoremInfos` 📖	CompOp	—
`decorateError` 📖	CompOp	—
`formatLemmas` 📖	CompOp	—
`isCondition` 📖	CompOp	—
`isSimpEq` 📖	CompOp	—
`isSimpTheorem` 📖	CompOp	—
`simpComm` 📖	CompOp	—
`simpNF` 📖	CompOp	—
`simpVarHead` 📖	CompOp	—
`withSimpTheoremInfos` 📖	CompOp	—

Batteries.Tactic.Lint.SimpTheoremInfo

Definitions

Name	Category	Theorems
`hyps` 📖	CompOp	—
`lhs` 📖	CompOp	—
`rhs` 📖	CompOp	—

Lean.Meta.DiscrTree

Definitions

Name	Category	Theorems
`elements` 📖	CompOp	—

LibraryNote

Definitions

Name	Category	Theorems
`«simp-normal_form»` 📖	CompOp	—

---

← Back to Index