ToExpr

📁 Source: Mathlib/Tactic/ToExpr.lean

Statistics

Metric	Count
Definitions instToExprBinderInfo_mathlib, toExpr, instToExprExpr_mathlib, toExpr, instToExprLevelMVarId_mathlib, toExpr, instToExprLevel_mathlib, toExpr, instToExprMData_mathlib, instToExprMVarId_mathlib, toExpr, instToExprPUnitOfToLevel_mathlib, instToExprRaw_mathlib, toExpr, instToExprRaw_mathlib_1, toExpr, instToExprSourceInfo_mathlib, toExpr, instToExprSyntax_mathlib, toExpr, instToExprULift_mathlib, toExpr	22
Theorems	0
Total	22

Mathlib

Definitions

Name	Category	Theorems
instToExprBinderInfo_mathlib 📖	CompOp	—
instToExprExpr_mathlib 📖	CompOp	—
instToExprLevelMVarId_mathlib 📖	CompOp	—
instToExprLevel_mathlib 📖	CompOp	—
instToExprMData_mathlib 📖	CompOp	—
instToExprMVarId_mathlib 📖	CompOp	—
instToExprPUnitOfToLevel_mathlib 📖	CompOp	—
instToExprRaw_mathlib 📖	CompOp	—
instToExprRaw_mathlib_1 📖	CompOp	—
instToExprSourceInfo_mathlib 📖	CompOp	—
instToExprSyntax_mathlib 📖	CompOp	—
instToExprULift_mathlib 📖	CompOp	—

Mathlib.instToExprBinderInfo_mathlib

Definitions

Name	Category	Theorems
toExpr 📖	CompOp	—

Mathlib.instToExprExpr_mathlib

Definitions

Name	Category	Theorems
toExpr 📖	CompOp	—

Mathlib.instToExprLevelMVarId_mathlib

Definitions

Name	Category	Theorems
toExpr 📖	CompOp	—

Mathlib.instToExprLevel_mathlib

Definitions

Name	Category	Theorems
toExpr 📖	CompOp	—

Mathlib.instToExprMVarId_mathlib

Definitions

Name	Category	Theorems
toExpr 📖	CompOp	—

Mathlib.instToExprRaw_mathlib

Definitions

Name	Category	Theorems
toExpr 📖	CompOp	—

Mathlib.instToExprRaw_mathlib_1

Definitions

Name	Category	Theorems
toExpr 📖	CompOp	—

Mathlib.instToExprSourceInfo_mathlib

Definitions

Name	Category	Theorems
toExpr 📖	CompOp	—

Mathlib.instToExprSyntax_mathlib

Definitions

Name	Category	Theorems
toExpr 📖	CompOp	—

Mathlib.instToExprULift_mathlib

Definitions

Name	Category	Theorems
toExpr 📖	CompOp	—

---

← Back to Index