Commit 2024-10-13 11:16 81d66bb8
View on Github →chore: more adaptations for lean4#5542 (#17688)
In [lean4#5542](https://github.com/leanprover/lean4/pull/5542) we are deprecating inductive ... :=, structure ... :=, and class ... := for their ... where counterparts. Continuation of #17655.