search

leanprover-community / mathport

Mathport is a tool for porting Lean3 projects to Lean4
Apache License 2.0
41 stars 15 forks source link

`simp` often gets the wrong direction #164

Closed gebner closed 2 years ago

gebner commented 2 years ago

I often see simp [← Int.neg_neg] in the synport, where the Lean 3 version was simp [int.neg_neg].