- 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 subexpressione
in the other (at the same position), we consider?x
equal toe
.
Instances For
- 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
.
Instances For
@[reducible, inline]
Equations
Instances For
@[always_inline]
def
Aesop.EqualUpToIdsM.run'
{α : Type}
(x : EqualUpToIdsM α)
(commonMCtx? : Option Lean.MetavarContext)
(mctx₁ mctx₂ : Lean.MetavarContext)
(allowAssignmentDiff : Bool)
:
Lean.MetaM (α × State)
Equations
Instances For
def
Aesop.EqualUpToIdsM.run
{α : Type}
(x : EqualUpToIdsM α)
(commonMCtx? : Option Lean.MetavarContext)
(mctx₁ mctx₂ : Lean.MetavarContext)
(allowAssignmentDiff : Bool)
:
Equations
Instances For
@[inline]
Equations
- Aesop.EqualUpToIds.readCommonMCtx? = do let __do_lift ← read pure __do_lift.commonMCtx?
Instances For
@[inline]
Equations
- Aesop.EqualUpToIds.readMCtx₁ = do let __do_lift ← read pure __do_lift.mctx₁
Instances For
@[inline]
Equations
- Aesop.EqualUpToIds.readMCtx₂ = do let __do_lift ← read pure __do_lift.mctx₂
Instances For
@[inline]
Equations
- Aesop.EqualUpToIds.readAllowAssignmentDiff = do let __do_lift ← read pure __do_lift.allowAssignmentDiff
Instances For
@[specialize #[]]
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[specialize #[]]
Equations
- One or more equations did not get rendered due to their size.
Instances For
- lctx₁ : Lean.LocalContext
- localInstances₁ : Lean.LocalInstances
- lctx₂ : Lean.LocalContext
- localInstances₂ : Lean.LocalInstances
- equalFVarIds : Std.HashMap Lean.FVarId Lean.FVarId
Instances For
- mvarId (mvarId : Lean.MVarId) : MVarValue
- expr (e : Lean.Expr) : MVarValue
- delayedAssignment (da : Lean.DelayedMetavarAssignment) : MVarValue
Instances For
@[specialize #[]]
Equations
Instances For
@[specialize #[]]
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
Instances For
@[implemented_by Aesop.EqualUpToIds.Unsafe.levelsEqualUpToIdsCore]
@[reducible, inline]
Equations
Instances For
@[specialize #[]]
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[specialize #[]]
Equations
- One or more equations did not get rendered due to their size.
Instances For
unsafe def
Aesop.EqualUpToIds.Unsafe.exprsEqualUpToIdsCore₂.printExpr
(mctx : Lean.MetavarContext)
(lctx : Lean.LocalContext)
(localInstances : Lean.LocalInstances)
(e : Lean.Expr)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[specialize #[]]
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
Instances For
unsafe def
Aesop.EqualUpToIds.Unsafe.exprsEqualUpToIdsCore₃.normalizeMVar
(mctx : Lean.MetavarContext)
(m : Lean.MVarId)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
- Aesop.EqualUpToIds.Unsafe.exprsEqualUpToIdsCore₃.compareMVarValues x✝¹ x✝ = pure false
Instances For
@[specialize #[]]
Equations
- One or more equations did not get rendered due to their size.
- Aesop.EqualUpToIds.Unsafe.localDeclsEqualUpToIdsCore x✝¹ x✝ = pure false
Instances For
@[specialize #[]]
unsafe def
Aesop.EqualUpToIds.Unsafe.localContextsEqualUpToIdsCore
(lctx₁ lctx₂ : Lean.LocalContext)
(localInstances₁ localInstances₂ : Lean.LocalInstances)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
unsafe def
Aesop.EqualUpToIds.Unsafe.localContextsEqualUpToIdsCore.go
(decls₁ decls₂ : Array Lean.LocalDecl)
(h : decls₁.size = decls₂.size)
(i : Nat)
(gctx : GoalContext)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[specialize #[]]
unsafe def
Aesop.EqualUpToIds.Unsafe.unassignedMVarsEqualUpToIdsCore
(mvarId₁ mvarId₂ : Lean.MVarId)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[implemented_by Aesop.EqualUpToIds.Unsafe.exprsEqualUpToIdsCore₁]
@[implemented_by Aesop.EqualUpToIds.Unsafe.unassignedMVarsEqualUpToIdsCore]
@[specialize #[]]
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Aesop.exprsEqualUpToIds
(mctx₁ mctx₂ : Lean.MetavarContext)
(lctx₁ lctx₂ : Lean.LocalContext)
(localInstances₁ localInstances₂ : Lean.LocalInstances)
(e₁ e₂ : Lean.Expr)
(allowAssignmentDiff : Bool := false)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Aesop.unassignedMVarsEqualUptoIds
(commonMCtx? : Option Lean.MetavarContext)
(mctx₁ mctx₂ : Lean.MetavarContext)
(mvarId₁ mvarId₂ : Lean.MVarId)
(allowAssignmentDiff : Bool := false)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Aesop.unassignedMVarsEqualUptoIds'
(commonMCtx? : Option Lean.MetavarContext)
(mctx₁ mctx₂ : Lean.MetavarContext)
(mvarId₁ mvarId₂ : Lean.MVarId)
(allowAssignmentDiff : Bool := false)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Aesop.tacticStatesEqualUpToIds
(commonMCtx? : Option Lean.MetavarContext)
(mctx₁ mctx₂ : Lean.MetavarContext)
(goals₁ goals₂ : Array Lean.MVarId)
(allowAssignmentDiff : Bool := false)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Aesop.tacticStatesEqualUpToIds'
(commonMCtx? : Option Lean.MetavarContext)
(mctx₁ mctx₂ : Lean.MetavarContext)
(goals₁ goals₂ : Array Lean.MVarId)
(allowAssignmentDiff : Bool := false)
:
Equations
- One or more equations did not get rendered due to their size.