We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
The notation for abs clashes with some variants of the match notation:
abs
import Mathbin.Algebra.Abs -- works if this is not imported def test : Nat → Nat | 0 => 0 -- expected '|' | n + 1 => 0
The text was updated successfully, but these errors were encountered:
Discussion on zulip: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Mathport.20abs.20syntax.20clash
Sorry, something went wrong.
fix: disable |·| notation
4b005f6
See #73.
Transferred to mathlib4 because we've solved the issue in mathport (by just ignoring the notation).
mathlib4
We still need to figure out a notation for the absolute value in Lean 4 though.
#477 added the |abs| notation.
No branches or pull requests
The notation for
abs
clashes with some variants of the match notation:The text was updated successfully, but these errors were encountered: