Zulip Chat Archive
Stream: mathlib4
Topic: abs notation breaks unif_hint
Eric Wieser (Jan 16 2024 at 11:55):
The following fails unless you comment out the import:
import Mathlib.Algebra.Order.Group.Abs
unif_hint where
|-
1 =?= 1
Last updated: May 02 2025 at 03:31 UTC