Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
feat: add double parens abbreviations (#523)
Corresponds to [[ and {{ -- they aren't used (yet) in Mathlib but would potentially be used for LaurentSeries notation.
- Loading branch information