search

leanprover / lean3-mode

Emacs mode for Lean
Apache License 2.0
69 stars 17 forks source link

Abbreviations `\/` and `\quot` for `⧸` #38

Closed Vierkantor closed 2 years ago

Vierkantor commented 2 years ago

Mathlib PR 10501 introduces ⧸ as an infix operator producing quotient types. I propose that we use \/ and \quot as abbreviations for this operator.