max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: add temporary workaround

Browse source
This commit is contained in:
Leonardo de Moura 2024-02-18 13:28:25 -08:00 • committed by Leonardo de Moura
parent ead14987bc
commit 55ce5d570c
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Init/Data/Int/DivModLemmas.lean
View file

@ -343,5 +343,5 @@ def bmod (x : Int) (m : Nat) : Int :=
r - m
@[simp] theorem bmod_emod : bmod x m % m = x % m := by
dsimp [bmod]
simp [bmod] -- TODO (zeta): It was `dsimp`
split <;> simp [Int.sub_emod]