fix: add matrix notation stub for mathport (#3429)

Part of the implementation of mathport support for the `matrix.notation` user notation, see [Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/!4.233215.20and.20data.2Ematrix.2Enotation/near/349219891).
leanprover-community · Apr 13, 2023 · dfbb8aa · dfbb8aa
1 parent 94c39a2
commit dfbb8aa
Showing 1 changed file with 9 additions and 0 deletions.
diff --git a/Mathlib/Mathport/Syntax.lean b/Mathlib/Mathport/Syntax.lean
@@ -354,3 +354,12 @@ namespace Command
 /- E -/ syntax (name := assertNoInstance) "assert_no_instance " term : command
 
 end Command
+
+namespace Term
+
+/- M -/ syntax (name := matrixNotation)
+  "!![" sepBy1(term,+,?, ";", "; ", allowTrailingSep) "]" : term
+/- M -/ syntax (name := matrixNotationRx0) "!![" ";"* "]" : term
+/- M -/ syntax (name := matrixNotation0xC) "!![" ","+ "]" : term
+
+end Term