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)

@[implicit_reducible, always_inline]

instance Aesop.instMonadEqualUpToIdsM : Monad EqualUpToIdsM

Equations

• Aesop.instMonadEqualUpToIdsM = inferInstance

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

Equations

• x.run' commonMCtx? mctx₁ mctx₂ allowAssignmentDiff = (x { commonMCtx? := commonMCtx?, mctx₁ := mctx₁, mctx₂ := mctx₂, allowAssignmentDiff := allowAssignmentDiff }).run { }

def Aesop.EqualUpToIdsM.run {α : Type} (x : EqualUpToIdsM α) (commonMCtx? : Option Lean.MetavarContext) (mctx₁ 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? : EqualUpToIdsM (Option Lean.MetavarContext)

Equations

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

@[inline]

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

Equations

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

@[inline]

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

Equations

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

@[inline]

def Aesop.EqualUpToIds.readAllowAssignmentDiff : EqualUpToIdsM Bool

Equations

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

@[specialize #[]]

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

Equations

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

@[specialize #[]]

def Aesop.EqualUpToIds.equalCommonMVars? (mvarId₁ mvarId₂ : Lean.MVarId) : 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 (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

Equations

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

@[specialize #[]]

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

Equations

• One or more equations did not get rendered due to their size.
• Aesop.EqualUpToIds.Unsafe.levelsEqualUpToIdsCore' Lean.Level.zero Lean.Level.zero = pure true
• Aesop.EqualUpToIds.Unsafe.levelsEqualUpToIdsCore' l₁.succ l₂.succ = Aesop.EqualUpToIds.Unsafe.levelsEqualUpToIdsCore l₁ l₂
• Aesop.EqualUpToIds.Unsafe.levelsEqualUpToIdsCore' (l₁.max m₁) (l₂.max m₂) = (Aesop.EqualUpToIds.Unsafe.levelsEqualUpToIdsCore l₁ l₂ <&&> Aesop.EqualUpToIds.Unsafe.levelsEqualUpToIdsCore m₁ m₂)
• Aesop.EqualUpToIds.Unsafe.levelsEqualUpToIdsCore' (l₁.imax m₁) (l₂.imax m₂) = (Aesop.EqualUpToIds.Unsafe.levelsEqualUpToIdsCore l₁ l₂ <&&> Aesop.EqualUpToIds.Unsafe.levelsEqualUpToIdsCore m₁ m₂)
• Aesop.EqualUpToIds.Unsafe.levelsEqualUpToIdsCore' (Lean.Level.param n₁) (Lean.Level.param n₂) = pure (n₁ == n₂)
• Aesop.EqualUpToIds.Unsafe.levelsEqualUpToIdsCore' x✝¹ x✝ = pure false

@[implemented_by Aesop.EqualUpToIds.Unsafe.levelsEqualUpToIdsCore]

opaque Aesop.EqualUpToIds.levelsEqualUpToIdsCore (l₁ l₂ : Lean.Level) : 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₁ e₂ : Lean.Expr) : ReaderT GoalContext EqualUpToIdsM Bool

Equations

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

@[specialize #[]]

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

Equations

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

@[specialize #[]]

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

Equations

• One or more equations did not get rendered due to their size.
• Aesop.EqualUpToIds.Unsafe.exprsEqualUpToIdsCore₃ (Lean.Expr.bvar i) (Lean.Expr.bvar j) = pure (i == j)
• Aesop.EqualUpToIds.Unsafe.exprsEqualUpToIdsCore₃ (Lean.Expr.sort u) (Lean.Expr.sort v) = liftM (Aesop.EqualUpToIds.Unsafe.levelsEqualUpToIdsCore u v)
• Aesop.EqualUpToIds.Unsafe.exprsEqualUpToIdsCore₃ (f₁.app x₁) (f₂.app x₂) = (Aesop.EqualUpToIds.Unsafe.exprsEqualUpToIdsCore₂ f₁ f₂ <&&> Aesop.EqualUpToIds.Unsafe.exprsEqualUpToIdsCore₂ x₁ x₂)
• Aesop.EqualUpToIds.Unsafe.exprsEqualUpToIdsCore₃ (Lean.Expr.lit l₁) (Lean.Expr.lit l₂) = pure (l₁ == l₂)
• Aesop.EqualUpToIds.Unsafe.exprsEqualUpToIdsCore₃ (Lean.Expr.mdata data e₁) x✝ = Aesop.EqualUpToIds.Unsafe.exprsEqualUpToIdsCore₂ e₁ x✝
• Aesop.EqualUpToIds.Unsafe.exprsEqualUpToIdsCore₃ x✝ (Lean.Expr.mdata data e₂) = Aesop.EqualUpToIds.Unsafe.exprsEqualUpToIdsCore₂ x✝ e₂
• Aesop.EqualUpToIds.Unsafe.exprsEqualUpToIdsCore₃ (Lean.Expr.proj n₁ i₁ e₁) (Lean.Expr.proj n₂ i₂ e₂) = (pure (n₁ == n₂ && i₁ == i₂) <&&> Aesop.EqualUpToIds.Unsafe.exprsEqualUpToIdsCore₂ e₁ e₂)
• Aesop.EqualUpToIds.Unsafe.exprsEqualUpToIdsCore₃ x✝¹ x✝ = pure false

@[specialize #[]]

unsafe def Aesop.EqualUpToIds.Unsafe.localDeclsEqualUpToIdsCore (ldecl₁ ldecl₂ : Lean.LocalDecl) : ReaderT GoalContext EqualUpToIdsM Bool

Equations

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

@[specialize #[]]

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

Equations

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

@[specialize #[]]

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

Equations

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

@[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

Equations

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

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

Equations

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

def Aesop.exprsEqualUpToIds' (e₁ e₂ : Lean.Expr) (allowAssignmentDiff : 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₁ mctx₂ : Lean.MetavarContext) (mvarId₁ mvarId₂ : Lean.MVarId) (allowAssignmentDiff : 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₁ mctx₂ : Lean.MetavarContext) (mvarId₁ mvarId₂ : Lean.MVarId) (allowAssignmentDiff : Bool := false) : Lean.MetaM (Bool × EqualUpToIdsM.State)

Equations

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

def Aesop.tacticStatesEqualUpToIds (commonMCtx? : Option Lean.MetavarContext) (mctx₁ mctx₂ : Lean.MetavarContext) (goals₁ goals₂ : Array Lean.MVarId) (allowAssignmentDiff : 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₁ mctx₂ : Lean.MetavarContext) (goals₁ goals₂ : Array Lean.MVarId) (allowAssignmentDiff : Bool := false) : Lean.MetaM (Bool × EqualUpToIdsM.State)

Equations

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