From adcfc58d385c5596e652ae50bcffbf3e697e222e Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Fri, 18 Mar 2022 00:28:27 +0000
Subject: [PATCH] chore(data/matrix/block): Do not print `matrix.from_blocks`
 with dot notation (#12774)

`A.from_blocks B C D` is weird and asymmetric compared to `from_blocks A B C D`. In future we might want to introduce notation.
---
 src/data/matrix/block.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/data/matrix/block.lean b/src/data/matrix/block.lean
index 44c6939dba1cb..433ae0260aeed 100644
--- a/src/data/matrix/block.lean
+++ b/src/data/matrix/block.lean
@@ -28,6 +28,7 @@ section block_matrices
 
 /-- We can form a single large matrix by flattening smaller 'block' matrices of compatible
 dimensions. -/
+@[pp_nodot]
 def from_blocks (A : matrix n l α) (B : matrix n m α) (C : matrix o l α) (D : matrix o m α) :
   matrix (n ⊕ o) (l ⊕ m) α :=
 sum.elim (λ i, sum.elim (A i) (B i))