From dfbb8aad777b5acef3b31f2c3edcc225fe6eea93 Mon Sep 17 00:00:00 2001
From: Mario Carneiro <di.gama@gmail.com>
Date: Thu, 13 Apr 2023 23:14:29 +0000
Subject: [PATCH] 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).
---
 Mathlib/Mathport/Syntax.lean | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/Mathlib/Mathport/Syntax.lean b/Mathlib/Mathport/Syntax.lean
index bb8beb39e43b6..c13dd18f2b10e 100644
--- 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