mirefek
mirefek
I think it is correct. In my view, the general rule would be that if there are 4 lines a, b, c, d, then a ⟂ b & c ⟂...
I have also noticed this bug. I am closing my issue https://github.com/google-deepmind/alphageometry/issues/20 since it is already a pull request (I haven't realized first).
Same for Emacs. Any idea what is causing that?
To be honest, I was not really sure where this should belong. I thought it was low-level enough that a potential user might not want Mathlib dependency. Batteries would feel...
I wonder if also the "unused variable `h`" warning could be prevented at the test ``` example (a b : Nat) (_h : a = b) : True := by...
We looked into it a bit with Eric, and it turns out the Linter is very basic -- only looks into the final proof term, and doesn't look into the...