Basic

📁 Source: Batteries/Lean/Meta/Basic.lean

Statistics

Metric	Count
Definitions eraseAssignment, getTypeCleanup, isDeclared, synthInstance, getUnassignedExprMVars, mkFreshIdWithPrefix, saturate1, sortFVarsByContextOrder, unhygienic, declareExprMVar, eraseExprMVarAssignment, getExprMVarDecl, isExprMVarAssignedOrDelayedAssigned, isExprMVarDeclared, unassignedExprMVars, instAlternativeMonadMetaM	16
Theorems	0
Total	16

Lean

Definitions

Name	Category	Theorems
instAlternativeMonadMetaM 📖	CompOp	—

Lean.MVarId

Definitions

Name	Category	Theorems
eraseAssignment 📖	CompOp	—
getTypeCleanup 📖	CompOp	—
isDeclared 📖	CompOp	—
synthInstance 📖	CompOp	—

Lean.Meta

Definitions

Name	Category	Theorems
getUnassignedExprMVars 📖	CompOp	—
mkFreshIdWithPrefix 📖	CompOp	—
saturate1 📖	CompOp	—
sortFVarsByContextOrder 📖	CompOp	—
unhygienic 📖	CompOp	—

Lean.MetavarContext

Definitions

Name	Category	Theorems
declareExprMVar 📖	CompOp	—
eraseExprMVarAssignment 📖	CompOp	—
getExprMVarDecl 📖	CompOp	—
isExprMVarAssignedOrDelayedAssigned 📖	CompOp	—
isExprMVarDeclared 📖	CompOp	—
unassignedExprMVars 📖	CompOp	—

---

← Back to Index