ToBatteries

📁 Source: Mathlib/Tactic/FunProp/ToBatteries.lean

Statistics

Metric	Count
Definitions swapBVars, betaThroughLet, etaExpand1, headBetaThroughLet, isOrderedSubsetOf, mkProdElem, mkProdProj, mkProdSplitElem, mkUncurryFun	9
Theorems	0
Total	9

Lean.Expr

Definitions

Name	Category	Theorems
swapBVars 📖	CompOp	—

Mathlib.Meta.FunProp

Definitions

Name	Category	Theorems
betaThroughLet 📖	CompOp	—
etaExpand1 📖	CompOp	—
headBetaThroughLet 📖	CompOp	—
isOrderedSubsetOf 📖	CompOp	—
mkProdElem 📖	CompOp	—
mkProdProj 📖	CompOp	—
mkProdSplitElem 📖	CompOp	—
mkUncurryFun 📖	CompOp	—

---

← Back to Index