search

hhu-adam / Robo

A game for learning lean 4 where a cute little Robo joins you on your exploration of the Mathiverse. The game is in German 🇩🇪
https://adam.math.hhu.de
Apache License 2.0
16 stars 9 forks source link

`by_contra` ignores `tactic.hygienic` #26

Open joneugster opened 4 months ago

joneugster commented 4 months ago

As with all tactics that are written as macros, it does not respect the option tactic.hygienic. This is a "bug" in Lean core, but we should raise an issue.

joneugster commented 4 months ago

by_cases is in the same boat.