ModEq notation borked after bump

Stream: mathlib4

[Kevin Buzzard]

This is presumably a result of the nodot change:

import Mathlib.Data.Nat.ModEq

#check 1 ≡ 2 [MOD 3] -- 1 ≡ 2 [MOD 3] : Prop

variable (a b c : ℕ) in
#check a ≡ b [MOD c] -- c.ModEq a b : Prop

(I'm sorry, I don't have a clue how to fix it, I'm just reporting)

[Ruben Van de Velde]

I suspect that will be fixed by changes that are in flight

[Kevin Buzzard]

I was proving ZHat lemmas :-)

[Kyle Miller]

In the meantime, you can turn off dot notation with set_option pp.fieldNotation.generalized false

[Kyle Miller]

(the official name for dot notation is "generalized field notation")

[Kyle Miller]

There's already a fix for this in what will be Lean 4.8.0-rc2 though