Aesop.Util.EqualUpToIds

source

structure Aesop.EqualUpToIds.EqualUpToIdsM.Context :

Type

Instances For

source

structure Aesop.EqualUpToIds.EqualUpToIdsM.State :

Type

equalMVarIds : Lean.HashMap Lean.MVarId Lean.MVarId
equalLMVarIds : Lean.HashMap Lean.LMVarId Lean.LMVarId

Instances For

source

@[reducible, inline]

abbrev Aesop.EqualUpToIds.EqualUpToIdsM (α : Type) :

Type

Equations

Aesop.EqualUpToIds.EqualUpToIdsM = ReaderT Aesop.EqualUpToIds.EqualUpToIdsM.Context (StateRefT' IO.RealWorld Aesop.EqualUpToIds.EqualUpToIdsM.State Lean.MetaM)

Instances For

source

def Aesop.EqualUpToIds.readCommonMCtx :

Aesop.EqualUpToIds.EqualUpToIdsM Lean.MetavarContext

Equations

Aesop.EqualUpToIds.readCommonMCtx = do let __do_lift ← read pure __do_lift.commonMCtx

Instances For

source

def Aesop.EqualUpToIds.readMCtx₁ :

Aesop.EqualUpToIds.EqualUpToIdsM Lean.MetavarContext

Equations

Aesop.EqualUpToIds.readMCtx₁ = do let __do_lift ← read pure __do_lift.mctx₁

Instances For

source

def Aesop.EqualUpToIds.readMCtx₂ :

Aesop.EqualUpToIds.EqualUpToIdsM Lean.MetavarContext

Equations

Aesop.EqualUpToIds.readMCtx₂ = do let __do_lift ← read pure __do_lift.mctx₂

Instances For

source

@[always_inline]

instance Aesop.EqualUpToIds.instMonadEqualUpToIdsM :

Monad Aesop.EqualUpToIds.EqualUpToIdsM

Equations

Aesop.EqualUpToIds.instMonadEqualUpToIdsM = let __src := inferInstanceAs (Monad Aesop.EqualUpToIds.EqualUpToIdsM); Monad.mk

source

def Aesop.EqualUpToIds.EqualUpToIdsM.run {α : Type} (x : Aesop.EqualUpToIds.EqualUpToIdsM α) (commonMCtx : Lean.MetavarContext) (mctx₁ : Lean.MetavarContext) (mctx₂ : Lean.MetavarContext) :

Lean.MetaM α

Equations

One or more equations did not get rendered due to their size.

Instances For

source

structure Aesop.EqualUpToIds.GoalContext :

Type

mdecl₁ : Lean.MetavarDecl
mdecl₂ : Lean.MetavarDecl
equalFVarIds : Lean.HashMap Lean.FVarId Lean.FVarId

Instances For

source

inductive Aesop.EqualUpToIds.MVarValue :

Type

mvarId: Lean.MVarId → Aesop.EqualUpToIds.MVarValue
expr: Lean.Expr → Aesop.EqualUpToIds.MVarValue
delayedAssignment: Lean.DelayedMetavarAssignment → Aesop.EqualUpToIds.MVarValue

Instances For

source

unsafe def Aesop.EqualUpToIds.Unsafe.levelsEqualUpToIdsCore (l₁ : Lean.Level) (l₂ : Lean.Level) :

Aesop.EqualUpToIds.EqualUpToIdsM Bool

Equations

Aesop.EqualUpToIds.Unsafe.levelsEqualUpToIdsCore l₁ l₂ = if ptrEq l₁ l₂ = true then pure true else Aesop.EqualUpToIds.Unsafe.levelsEqualUpToIdsCore' l₁ l₂

Instances For

source

unsafe def Aesop.EqualUpToIds.Unsafe.levelsEqualUpToIdsCore' :

Lean.Level → Lean.Level → Aesop.EqualUpToIds.EqualUpToIdsM Bool

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[implemented_by Aesop.EqualUpToIds.Unsafe.levelsEqualUpToIdsCore]

opaque Aesop.EqualUpToIds.levelsEqualUpToIdsCore (l₁ : Lean.Level) (l₂ : Lean.Level) :

Aesop.EqualUpToIds.EqualUpToIdsM Bool

source

unsafe def Aesop.EqualUpToIds.Unsafe.exprsEqualUpToIdsCore (e₁ : Lean.Expr) (e₂ : Lean.Expr) :

ReaderT Aesop.EqualUpToIds.GoalContext Aesop.EqualUpToIds.EqualUpToIdsM Bool

Equations

One or more equations did not get rendered due to their size.

Instances For

source

unsafe def Aesop.EqualUpToIds.Unsafe.exprsEqualUpToIdsCore.instMVars (mctx : Lean.MetavarContext) (e : Lean.Expr) :

Lean.MetaM Lean.Expr

Equations

Aesop.EqualUpToIds.Unsafe.exprsEqualUpToIdsCore.instMVars mctx e = Lean.Meta.withMCtx mctx (Lean.instantiateMVars e)

Instances For

source

unsafe def Aesop.EqualUpToIds.Unsafe.exprsEqualUpToIdsCore.printExpr (mctx : Lean.MetavarContext) (mdecl : Lean.MetavarDecl) (e : Lean.Expr) :

Lean.MetaM Lean.MessageData

Equations

One or more equations did not get rendered due to their size.

Instances For

source

unsafe def Aesop.EqualUpToIds.Unsafe.exprsEqualUpToIdsCore' :

Lean.Expr → Lean.Expr → ReaderT Aesop.EqualUpToIds.GoalContext Aesop.EqualUpToIds.EqualUpToIdsM Bool

Equations

One or more equations did not get rendered due to their size.

Instances For

source

unsafe def Aesop.EqualUpToIds.Unsafe.exprsEqualUpToIdsCore'.normalizeMVar (mctx : Lean.MetavarContext) (m : Lean.MVarId) :

Lean.MetaM Aesop.EqualUpToIds.MVarValue

Equations

One or more equations did not get rendered due to their size.

Instances For

source

unsafe def Aesop.EqualUpToIds.Unsafe.exprsEqualUpToIdsCore'.compareMVarValues (v₁ : Aesop.EqualUpToIds.MVarValue) (v₂ : Aesop.EqualUpToIds.MVarValue) :

ReaderT Aesop.EqualUpToIds.GoalContext Aesop.EqualUpToIds.EqualUpToIdsM Bool

Equations

One or more equations did not get rendered due to their size.

Instances For

source

unsafe def Aesop.EqualUpToIds.Unsafe.localDeclsEqualUpToIdsCore :

Lean.LocalDecl → Lean.LocalDecl → ReaderT Aesop.EqualUpToIds.GoalContext Aesop.EqualUpToIds.EqualUpToIdsM Bool

Equations

One or more equations did not get rendered due to their size.

Instances For

source

unsafe def Aesop.EqualUpToIds.Unsafe.localContextsEqualUpToIdsCore (mdecl₁ : Lean.MetavarDecl) (mdecl₂ : Lean.MetavarDecl) :

Aesop.EqualUpToIds.EqualUpToIdsM (Option Aesop.EqualUpToIds.GoalContext)

Equations

One or more equations did not get rendered due to their size.

Instances For

source

unsafe def Aesop.EqualUpToIds.Unsafe.localContextsEqualUpToIdsCore.go (decls₁ : Array Lean.LocalDecl) (decls₂ : Array Lean.LocalDecl) (h : decls₁.size = decls₂.size) (i : Nat) (gctx : Aesop.EqualUpToIds.GoalContext) :

Aesop.EqualUpToIds.EqualUpToIdsM (Option Aesop.EqualUpToIds.GoalContext)

Equations

One or more equations did not get rendered due to their size.

Instances For

source

unsafe def Aesop.EqualUpToIds.Unsafe.unassignedMVarsEqualUpToIdsCore (mvarId₁ : Lean.MVarId) (mvarId₂ : Lean.MVarId) :

Aesop.EqualUpToIds.EqualUpToIdsM Bool

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[implemented_by Aesop.EqualUpToIds.Unsafe.unassignedMVarsEqualUpToIdsCore]

opaque Aesop.EqualUpToIds.unassignedMVarsEqualUpToIdsCore (mvarId₁ : Lean.MVarId) (mvarId₂ : Lean.MVarId) :

Aesop.EqualUpToIds.EqualUpToIdsM Bool

source

def Aesop.EqualUpToIds.tacticStatesEqualUpToIdsCore (goals₁ : Array Lean.MVarId) (goals₂ : Array Lean.MVarId) :

Aesop.EqualUpToIds.EqualUpToIdsM Bool

Equations

One or more equations did not get rendered due to their size.

Instances For

source

def Aesop.unassignedMVarsEqualUptoIds (commonMCtx : Lean.MetavarContext) (mctx₁ : Lean.MetavarContext) (mctx₂ : Lean.MetavarContext) (mvarId₁ : Lean.MVarId) (mvarId₂ : Lean.MVarId) :

Lean.MetaM Bool

Equations

Aesop.unassignedMVarsEqualUptoIds commonMCtx mctx₁ mctx₂ mvarId₁ mvarId₂ = (Aesop.EqualUpToIds.unassignedMVarsEqualUpToIdsCore mvarId₁ mvarId₂).run commonMCtx mctx₁ mctx₂

Instances For

source

def Aesop.tacticStatesEqualUpToIds (commonMCtx : Lean.MetavarContext) (mctx₁ : Lean.MetavarContext) (mctx₂ : Lean.MetavarContext) (goals₁ : Array Lean.MVarId) (goals₂ : Array Lean.MVarId) :

Lean.MetaM Bool

Equations

Aesop.tacticStatesEqualUpToIds commonMCtx mctx₁ mctx₂ goals₁ goals₂ = (Aesop.EqualUpToIds.tacticStatesEqualUpToIdsCore goals₁ goals₂).run commonMCtx mctx₁ mctx₂

Instances For

source

def Aesop.runTacticMCapturingPostState (t : Lean.Elab.Tactic.TacticM Unit) (preState : Lean.Meta.SavedState) (preGoals : List Lean.MVarId) :

Lean.MetaM (Lean.Meta.SavedState × List Lean.MVarId)

Equations

One or more equations did not get rendered due to their size.

Instances For