Documentation Verification Report

EqualUpToIds

📁 Source: Aesop/Util/EqualUpToIds.lean

Statistics

Metric	Count
Definitions `ExprsEqualUpToIdsM`, `GoalContext`, `equalFVarIds`, `lctx₁`, `lctx₂`, `localInstances₁`, `localInstances₂`, `MVarValue`, `exprsEqualUpToIdsCore₁`, `exprsEqualUpToIdsCore₂`, `exprsEqualUpToIdsCore₃`, `levelsEqualUpToIdsCore`, `levelsEqualUpToIdsCore'`, `localContextsEqualUpToIdsCore`, `localDeclsEqualUpToIdsCore`, `unassignedMVarsEqualUpToIdsCore`, `equalCommonLMVars?`, `equalCommonMVars?`, `exprsEqualUpToIdsCore`, `levelsEqualUpToIdsCore`, `readAllowAssignmentDiff`, `readCommonMCtx?`, `readMCtx₁`, `readMCtx₂`, `tacticStatesEqualUpToIdsCore`, `unassignedMVarsEqualUpToIdsCore`, `EqualUpToIdsM`, `Context`, `allowAssignmentDiff`, `commonMCtx?`, `mctx₁`, `mctx₂`, `equalLMVarIds`, `equalMVarIds`, `leftUnassignedMVarValues`, `rightUnassignedMVarValues`, `run`, `run'`, `exprsEqualUpToIds`, `exprsEqualUpToIds'`, `instMonadEqualUpToIdsM`, `tacticStatesEqualUpToIds`, `tacticStatesEqualUpToIds'`, `unassignedMVarsEqualUptoIds`, `unassignedMVarsEqualUptoIds'`	45
Theorems	0
Total	45

Aesop

Definitions

Name	Category	Theorems
`EqualUpToIdsM` 📖	CompOp	—
`exprsEqualUpToIds` 📖	CompOp	—
`exprsEqualUpToIds'` 📖	CompOp	—
`instMonadEqualUpToIdsM` 📖	CompOp	—
`tacticStatesEqualUpToIds` 📖	CompOp	—
`tacticStatesEqualUpToIds'` 📖	CompOp	—
`unassignedMVarsEqualUptoIds` 📖	CompOp	—
`unassignedMVarsEqualUptoIds'` 📖	CompOp	—

Aesop.EqualUpToIds

Definitions

Name	Category	Theorems
`ExprsEqualUpToIdsM` 📖	CompOp	—
`GoalContext` 📖	CompData	—
`MVarValue` 📖	CompData	—
`equalCommonLMVars?` 📖	CompOp	—
`equalCommonMVars?` 📖	CompOp	—
`exprsEqualUpToIdsCore` 📖	CompOp	—
`levelsEqualUpToIdsCore` 📖	CompOp	—
`readAllowAssignmentDiff` 📖	CompOp	—
`readCommonMCtx?` 📖	CompOp	—
`readMCtx₁` 📖	CompOp	—
`readMCtx₂` 📖	CompOp	—
`tacticStatesEqualUpToIdsCore` 📖	CompOp	—
`unassignedMVarsEqualUpToIdsCore` 📖	CompOp	—

Aesop.EqualUpToIds.GoalContext

Definitions

Name	Category	Theorems
`equalFVarIds` 📖	CompOp	—
`lctx₁` 📖	CompOp	—
`lctx₂` 📖	CompOp	—
`localInstances₁` 📖	CompOp	—
`localInstances₂` 📖	CompOp	—

Aesop.EqualUpToIds.Unsafe

Definitions

Name	Category	Theorems
`exprsEqualUpToIdsCore₁` 📖	CompOp	—
`exprsEqualUpToIdsCore₂` 📖	CompOp	—
`exprsEqualUpToIdsCore₃` 📖	CompOp	—
`levelsEqualUpToIdsCore` 📖	CompOp	—
`levelsEqualUpToIdsCore'` 📖	CompOp	—
`localContextsEqualUpToIdsCore` 📖	CompOp	—
`localDeclsEqualUpToIdsCore` 📖	CompOp	—
`unassignedMVarsEqualUpToIdsCore` 📖	CompOp	—

Aesop.EqualUpToIdsM

Definitions

Name	Category	Theorems
`Context` 📖	CompData	—
`run` 📖	CompOp	—
`run'` 📖	CompOp	—

Aesop.EqualUpToIdsM.Context

Definitions

Name	Category	Theorems
`allowAssignmentDiff` 📖	CompOp	—
`commonMCtx?` 📖	CompOp	—
`mctx₁` 📖	CompOp	—
`mctx₂` 📖	CompOp	—

Aesop.EqualUpToIdsM.State

Definitions

Name	Category	Theorems
`equalLMVarIds` 📖	CompOp	—
`equalMVarIds` 📖	CompOp	—
`leftUnassignedMVarValues` 📖	CompOp	—
`rightUnassignedMVarValues` 📖	CompOp	—

---

← Back to Index