CongrExclamation
📁 Source: Mathlib/Tactic/CongrExclamation.lean
Statistics
| Metric | Count |
|---|---|
DefinitionsConfig, beqEq, closePost, closePre, etaExpand, maxArgs, maxArgsFor, numArgsOk, partialApp, preTransparency, preferLHS, sameFun, transparency, typeEqs, unfoldSameFun, useCongrSimp, congr!, elabConfig, plausiblyEqualTypes, CongrMetaM, nextPattern, CongrState, goals, patterns, beqInst?, congrCore!, congrImplies?', congrN!, congrPasses!, congrPi?, congrSimp?, introsClean, obviousFunext?, obviousHfunext?, postCongr!, preCongr!, smartHCongr?, subsingletonHelim?, userCongr? | 39 |
| Theorems | 0 |
| Total | 39 |
Congr!
Definitions
| Name | Category | Theorems |
|---|---|---|
Config 📖 | CompData | — |
congr! 📖 | CompOp | — |
elabConfig 📖 | CompOp | — |
plausiblyEqualTypes 📖 | CompOp | — |
Congr!.Config
Definitions
| Name | Category | Theorems |
|---|---|---|
beqEq 📖 | CompOp | — |
closePost 📖 | CompOp | — |
closePre 📖 | CompOp | — |
etaExpand 📖 | CompOp | — |
maxArgs 📖 | CompOp | — |
maxArgsFor 📖 | CompOp | — |
numArgsOk 📖 | CompOp | — |
partialApp 📖 | CompOp | — |
preTransparency 📖 | CompOp | — |
preferLHS 📖 | CompOp | — |
sameFun 📖 | CompOp | — |
transparency 📖 | CompOp | — |
typeEqs 📖 | CompOp | — |
unfoldSameFun 📖 | CompOp | — |
useCongrSimp 📖 | CompOp | — |
CongrMetaM
Definitions
| Name | Category | Theorems |
|---|---|---|
nextPattern 📖 | CompOp | — |
CongrState
Definitions
| Name | Category | Theorems |
|---|---|---|
goals 📖 | CompOp | — |
patterns 📖 | CompOp | — |
Lean.MVarId
Definitions
| Name | Category | Theorems |
|---|---|---|
beqInst? 📖 | CompOp | — |
congrCore! 📖 | CompOp | — |
congrImplies?' 📖 | CompOp | — |
congrN! 📖 | CompOp | — |
congrPasses! 📖 | CompOp | — |
congrPi? 📖 | CompOp | — |
congrSimp? 📖 | CompOp | — |
introsClean 📖 | CompOp | — |
obviousFunext? 📖 | CompOp | — |
obviousHfunext? 📖 | CompOp | — |
postCongr! 📖 | CompOp | — |
preCongr! 📖 | CompOp | — |
smartHCongr? 📖 | CompOp | — |
subsingletonHelim? 📖 | CompOp | — |
userCongr? 📖 | CompOp | — |
(root)
Definitions
| Name | Category | Theorems |
|---|---|---|
CongrMetaM 📖 | CompOp | — |
CongrState 📖 | CompData | — |
---