Def Mathlib.Meta.SetNotationForOrder.useSetNotationFor

Modification history

2026-05-12 10:45

Mathlib/Tactic/SetNotationForOrder.lean

feat: implementation of `@[use_set_notation_for_order]` (#37347) …

Added Mathlib.Meta.SetNotationForOrder.useSetNotationFor View on Github →