Skip to content

Commit

Permalink
fix: add 'squash' to 'norm_cast' attribute for 'Int.cast_negSucc' (#8365
Browse files Browse the repository at this point in the history
)

This is an attempt at fixing the following behavior of `norm_cast`.
```lean

example (n : ℤ) : (-37 : ℤ) = n := by
  norm_cast -- goal is `Int.negSucc 36 = n`
  sorry
```
See [this discussion](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/linarith.20fails.20in.20a.20simple.20example/near/401592369).
  • Loading branch information
MichaelStollBayreuth committed Nov 16, 2023
1 parent 52199f5 commit da342c7
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Mathlib/Data/Int/Cast/Basic.lean
Expand Up @@ -49,7 +49,7 @@ namespace Int

variable {R : Type u} [AddGroupWithOne R]

@[simp, norm_cast]
@[simp, norm_cast squash]
theorem cast_negSucc (n : ℕ) : (-[n+1] : R) = -(n + 1 : ℕ) :=
AddGroupWithOne.intCast_negSucc n
#align int.cast_neg_succ_of_nat Int.cast_negSuccₓ
Expand Down

0 comments on commit da342c7

Please sign in to comment.