Reorder
📁 Source: Mathlib/Tactic/Translate/Reorder.lean
Statistics
| Metric | Count |
|---|---|
DefinitionstranslateReorder, Reorder, argReorders, beq, isEmpty, perm, permute!, permuteUniv, range, reverse, toString, elabArgStx, elabReorder, guessReorder, instBEqReorder, instInhabitedReorder, default, instToMessageDataReorder, instToStringReorder, reorder, reorderForall, reorderLambda, reorderPart, quot | 24 |
| Theorems | 0 |
| Total | 24 |
Lean.Parser.Category
Definitions
| Name | Category | Theorems |
|---|---|---|
translateReorder 📖 | CompOp | — |
Mathlib.Tactic.Translate
Definitions
| Name | Category | Theorems |
|---|---|---|
Reorder 📖 | CompData | — |
elabArgStx 📖 | CompOp | — |
elabReorder 📖 | CompOp | — |
guessReorder 📖 | CompOp | — |
instBEqReorder 📖 | CompOp | — |
instInhabitedReorder 📖 | CompOp | — |
instToMessageDataReorder 📖 | CompOp | — |
instToStringReorder 📖 | CompOp | — |
reorder 📖 | CompOp | — |
reorderForall 📖 | CompOp | — |
reorderLambda 📖 | CompOp | — |
reorderPart 📖 | CompOp | — |
Mathlib.Tactic.Translate.Reorder
Definitions
| Name | Category | Theorems |
|---|---|---|
argReorders 📖 | CompOp | — |
beq 📖 | CompOp | — |
isEmpty 📖 | CompOp | — |
perm 📖 | CompOp | — |
permute! 📖 | CompOp | — |
permuteUniv 📖 | CompOp | — |
range 📖 | CompOp | — |
reverse 📖 | CompOp | — |
toString 📖 | CompOp | — |
Mathlib.Tactic.Translate.instInhabitedReorder
Definitions
| Name | Category | Theorems |
|---|---|---|
default 📖 | CompOp | — |
Mathlib.Tactic.Translate.translateReorder
Definitions
| Name | Category | Theorems |
|---|---|---|
quot 📖 | CompOp | — |
---