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

@[always_inline]

instance Aesop.instMonadEqualUpToIdsM : Monad EqualUpToIdsM

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

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

@[inline]

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

@[inline]

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

@[inline]

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

@[inline]

def Aesop.EqualUpToIds.readAllowAssignmentDiff : EqualUpToIdsM Bool

@[specialize #[]]

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

@[specialize #[]]

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

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 (mvarId : Lean.MVarId) : MVarValue
• expr (e : Lean.Expr) : MVarValue
• delayedAssignment (da : Lean.DelayedMetavarAssignment) : MVarValue

@[specialize #[]]

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

@[specialize #[]]

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

@[implemented_by Aesop.EqualUpToIds.Unsafe.levelsEqualUpToIdsCore]

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

@[reducible, inline]

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

@[specialize #[]]

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

@[specialize #[]]

unsafe def Aesop.EqualUpToIds.Unsafe.exprsEqualUpToIdsCore₂ (e₁ e₂ : Lean.Expr) : 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 → ExprsEqualUpToIdsM Bool

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

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

@[specialize #[]]

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

@[specialize #[]]

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

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

@[specialize #[]]

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

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

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

@[implemented_by Aesop.EqualUpToIds.Unsafe.unassignedMVarsEqualUpToIdsCore]

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

@[specialize #[]]

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

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

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

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

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

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

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