Lean.Meta.Offset

partial def Lean.Meta.evalNat :

Equations

Lean.Meta.evalNat.isNatProjInst c nargs = (nargs == 4 && (c == `Add.add || c == `Sub.sub || c == `Mul.mul) || nargs == 6 && (c == `HAdd.hAdd || c == `HSub.hSub || c == `HMul.hMul) || nargs == 3 && c == `OfNat.ofNat)

Equations

Lean.Meta.isDefEqOffset s t = let ifNatExpr := fun x => do let type ← Lean.Meta.inferType s let a ← Lean.Meta.withNewMCtxDepth (Lean.Meta.isExprDefEqAux type (Lean.mkConst `Nat)) if a = true then x else pure Lean.LBool.undef; let isDefEq := fun s t => ifNatExpr (toLBoolM (Lean.Meta.isExprDefEqAux s t)); do let a ← Lean.Meta.getConfig if (!a.offsetCnstrs) = true then pure Lean.LBool.undef else do let a ← Lean.Meta.isOffset s match a with | some (s, k₁) => do let a ← Lean.Meta.isOffset t match a with | some (t, k₂) => if (k₁ == k₂) = true then isDefEq s t else if k₁ < k₂ then do let a ← Lean.Meta.mkOffset t (k₂ - k₁) isDefEq s a else do let a ← Lean.Meta.mkOffset s (k₁ - k₂) isDefEq a t | none => do let a ← Lean.Meta.evalNat t match a with | some v₂ => if v₂ ≥ k₁ then isDefEq s (Lean.mkNatLit (v₂ - k₁)) else ifNatExpr (pure Lean.LBool.false) | none => pure Lean.LBool.undef | none => do let a ← Lean.Meta.evalNat s match a with | some v₁ => do let a ← Lean.Meta.isOffset t match a with | some (t, k₂) => if v₁ ≥ k₂ then isDefEq (Lean.mkNatLit (v₁ - k₂)) t else ifNatExpr (pure Lean.LBool.false) | none => do let a ← Lean.Meta.evalNat t match a with | some v₂ => ifNatExpr (pure (Bool.toLBool (v₁ == v₂))) | none => pure Lean.LBool.undef | none => pure Lean.LBool.undef