structure Aesop.EqualUpToIdsM.Context : Type

• commonMCtx? : Option Lean.MetavarContext
• mctx₁ : Lean.MetavarContext
• mctx₂ : Lean.MetavarContext
• allowAssignmentDiff : Bool

  Allow metavariables to be unassigned on one side of the comparison and assigned on the other. So when we compare two expressions and we encounter a metavariable ?x in one of them and a subexpression e in the other (at the same position), we consider ?x equal to e.

structure Aesop.EqualUpToIdsM.State : Type

• equalMVarIds : Std.HashMap Lean.MVarId Lean.MVarId
• equalLMVarIds : Std.HashMap Lean.LMVarId Lean.LMVarId
• leftUnassignedMVarValues : Std.HashMap Lean.MVarId Lean.Expr

  A map from metavariables which are unassigned in the left goal to their corresponding expression in the right goal. Only used when allowAssignmentDiff = true.

• rightUnassignedMVarValues : Std.HashMap Lean.MVarId Lean.Expr

  A map from metavariables which are unassigned in the right goal to their corresponding expression in the left goal. Only used when allowAssignmentDiff = true.

@[reducible, inline]

abbrev Aesop.EqualUpToIdsM (α : Type) : Type

Equations

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

Instances For

• Aesop.instMonadEqualUpToIdsM

@[always_inline]

instance Aesop.instMonadEqualUpToIdsM : Monad Aesop.EqualUpToIdsM

Equations

• Aesop.instMonadEqualUpToIdsM = Monad.mk

def Aesop.EqualUpToIdsM.run' {α : Type} (x : Aesop.EqualUpToIdsM α) (commonMCtx? : Option Lean.MetavarContext) (mctx₁ : Lean.MetavarContext) (mctx₂ : Lean.MetavarContext) (allowAssignmentDiff : Bool) : Lean.MetaM (α × Aesop.EqualUpToIdsM.State)

Equations

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

def Aesop.EqualUpToIdsM.run {α : Type} (x : Aesop.EqualUpToIdsM α) (commonMCtx? : Option Lean.MetavarContext) (mctx₁ : Lean.MetavarContext) (mctx₂ : Lean.MetavarContext) (allowAssignmentDiff : Bool) : Lean.MetaM α

Equations

• x.run commonMCtx? mctx₁ mctx₂ allowAssignmentDiff = (fun (x : α × Aesop.EqualUpToIdsM.State) => x.fst) <$> x.run' commonMCtx? mctx₁ mctx₂ allowAssignmentDiff

@[inline]

def Aesop.EqualUpToIds.readCommonMCtx? : Aesop.EqualUpToIdsM (Option Lean.MetavarContext)

Equations

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

@[inline]

def Aesop.EqualUpToIds.readMCtx₁ : Aesop.EqualUpToIdsM Lean.MetavarContext

Equations

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

@[inline]

def Aesop.EqualUpToIds.readMCtx₂ : Aesop.EqualUpToIdsM Lean.MetavarContext

Equations

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

@[inline]

def Aesop.EqualUpToIds.readAllowAssignmentDiff : Aesop.EqualUpToIdsM Bool

Equations

• Aesop.EqualUpToIds.readAllowAssignmentDiff = do let __do_lift ← read pure __do_lift.allowAssignmentDiff

@[specialize #[]]

def Aesop.EqualUpToIds.equalCommonLMVars? (lmvarId₁ : Lean.LMVarId) (lmvarId₂ : Lean.LMVarId) : Aesop.EqualUpToIdsM (Option Bool)

Equations

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

@[specialize #[]]

def Aesop.EqualUpToIds.equalCommonMVars? (mvarId₁ : Lean.MVarId) (mvarId₂ : Lean.MVarId) : Aesop.EqualUpToIdsM (Option Bool)

Equations

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

structure Aesop.EqualUpToIds.GoalContext : Type

• lctx₁ : Lean.LocalContext
• localInstances₁ : Lean.LocalInstances
• lctx₂ : Lean.LocalContext
• localInstances₂ : Lean.LocalInstances
• equalFVarIds : Std.HashMap Lean.FVarId Lean.FVarId

inductive Aesop.EqualUpToIds.MVarValue : Type

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

@[specialize #[]]

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

@[specialize #[]]

unsafe def Aesop.EqualUpToIds.Unsafe.levelsEqualUpToIdsCore' : Lean.Level → Lean.Level → Aesop.EqualUpToIdsM Bool

@[implemented_by Aesop.EqualUpToIds.Unsafe.levelsEqualUpToIdsCore]

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

@[reducible, inline]

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

Equations

• Aesop.EqualUpToIds.ExprsEqualUpToIdsM = Lean.MonadCacheT (Lean.ExprStructEq × Lean.ExprStructEq) Bool (ReaderT Aesop.EqualUpToIds.GoalContext Aesop.EqualUpToIdsM)

@[specialize #[]]

unsafe def Aesop.EqualUpToIds.Unsafe.exprsEqualUpToIdsCore₁ (e₁ : Lean.Expr) (e₂ : Lean.Expr) : ReaderT Aesop.EqualUpToIds.GoalContext Aesop.EqualUpToIdsM Bool

@[specialize #[]]

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

unsafe def Aesop.EqualUpToIds.Unsafe.exprsEqualUpToIdsCore₂.printExpr (mctx : Lean.MetavarContext) (lctx : Lean.LocalContext) (localInstances : Lean.LocalInstances) (e : Lean.Expr) : Lean.MetaM Lean.MessageData

@[specialize #[]]

unsafe def Aesop.EqualUpToIds.Unsafe.exprsEqualUpToIdsCore₃ : Lean.Expr → Lean.Expr → Aesop.EqualUpToIds.ExprsEqualUpToIdsM Bool

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

unsafe def Aesop.EqualUpToIds.Unsafe.exprsEqualUpToIdsCore₃.compareMVarValues : Aesop.EqualUpToIds.MVarValue → Aesop.EqualUpToIds.MVarValue → Aesop.EqualUpToIds.ExprsEqualUpToIdsM Bool

@[specialize #[]]

unsafe def Aesop.EqualUpToIds.Unsafe.localDeclsEqualUpToIdsCore : Lean.LocalDecl → Lean.LocalDecl → ReaderT Aesop.EqualUpToIds.GoalContext Aesop.EqualUpToIdsM Bool

@[specialize #[]]

unsafe def Aesop.EqualUpToIds.Unsafe.localContextsEqualUpToIdsCore (lctx₁ : Lean.LocalContext) (lctx₂ : Lean.LocalContext) (localInstances₁ : Lean.LocalInstances) (localInstances₂ : Lean.LocalInstances) : Aesop.EqualUpToIdsM (Option Aesop.EqualUpToIds.GoalContext)

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.EqualUpToIdsM (Option Aesop.EqualUpToIds.GoalContext)

@[specialize #[]]

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

@[implemented_by Aesop.EqualUpToIds.Unsafe.exprsEqualUpToIdsCore₁]

opaque Aesop.EqualUpToIds.exprsEqualUpToIdsCore (e₁ : Lean.Expr) (e₂ : Lean.Expr) : ReaderT Aesop.EqualUpToIds.GoalContext Aesop.EqualUpToIdsM Bool

@[implemented_by Aesop.EqualUpToIds.Unsafe.unassignedMVarsEqualUpToIdsCore]

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

@[specialize #[]]

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

Equations

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

def Aesop.exprsEqualUpToIds (mctx₁ : Lean.MetavarContext) (mctx₂ : Lean.MetavarContext) (lctx₁ : Lean.LocalContext) (lctx₂ : Lean.LocalContext) (localInstances₁ : Lean.LocalInstances) (localInstances₂ : Lean.LocalInstances) (e₁ : Lean.Expr) (e₂ : Lean.Expr) (allowAssignmentDiff : optParam Bool false) : Lean.MetaM Bool

Equations

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

def Aesop.exprsEqualUpToIds' (e₁ : Lean.Expr) (e₂ : Lean.Expr) (allowAssignmentDiff : optParam Bool false) : Lean.MetaM Bool

Equations

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

def Aesop.unassignedMVarsEqualUptoIds (commonMCtx? : Option Lean.MetavarContext) (mctx₁ : Lean.MetavarContext) (mctx₂ : Lean.MetavarContext) (mvarId₁ : Lean.MVarId) (mvarId₂ : Lean.MVarId) (allowAssignmentDiff : optParam Bool false) : Lean.MetaM Bool

Equations

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

def Aesop.unassignedMVarsEqualUptoIds' (commonMCtx? : Option Lean.MetavarContext) (mctx₁ : Lean.MetavarContext) (mctx₂ : Lean.MetavarContext) (mvarId₁ : Lean.MVarId) (mvarId₂ : Lean.MVarId) (allowAssignmentDiff : optParam Bool false) : Lean.MetaM (Bool × Aesop.EqualUpToIdsM.State)

Equations

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

def Aesop.tacticStatesEqualUpToIds (commonMCtx? : Option Lean.MetavarContext) (mctx₁ : Lean.MetavarContext) (mctx₂ : Lean.MetavarContext) (goals₁ : Array Lean.MVarId) (goals₂ : Array Lean.MVarId) (allowAssignmentDiff : optParam Bool false) : Lean.MetaM Bool

Equations

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

def Aesop.tacticStatesEqualUpToIds' (commonMCtx? : Option Lean.MetavarContext) (mctx₁ : Lean.MetavarContext) (mctx₂ : Lean.MetavarContext) (goals₁ : Array Lean.MVarId) (goals₂ : Array Lean.MVarId) (allowAssignmentDiff : optParam Bool false) : Lean.MetaM (Bool × Aesop.EqualUpToIdsM.State)

Equations

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