From cc8a5581d64ed746775917285bb087355e704c9a Mon Sep 17 00:00:00 2001 From: Jakob von Raumer Date: Thu, 26 Nov 2015 16:16:29 +0000 Subject: [PATCH] chore(hott/cubical): add lost space hints around square concatenations --- hott/cubical/square.hlean | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/hott/cubical/square.hlean b/hott/cubical/square.hlean index 1d3cd96e7..3777f6d2c 100644 --- a/hott/cubical/square.hlean +++ b/hott/cubical/square.hlean @@ -82,12 +82,12 @@ namespace eq square p₁₀ p₁₂ p₀₁ p := by induction r; exact s₁₁ - infix `⬝h`:75 := hconcat --type using \tr - infix `⬝v`:75 := vconcat --type using \tr - infix `⬝hp`:75 := hconcat_eq --type using \tr - infix `⬝vp`:75 := vconcat_eq --type using \tr - infix `⬝ph`:75 := eq_hconcat --type using \tr - infix `⬝pv`:75 := eq_vconcat --type using \tr + infix ` ⬝h `:75 := hconcat --type using \tr + infix ` ⬝v `:75 := vconcat --type using \tr + infix ` ⬝hp `:75 := hconcat_eq --type using \tr + infix ` ⬝vp `:75 := vconcat_eq --type using \tr + infix ` ⬝ph `:75 := eq_hconcat --type using \tr + infix ` ⬝pv `:75 := eq_vconcat --type using \tr postfix `⁻¹ʰ`:(max+1) := hinverse --type using \-1h postfix `⁻¹ᵛ`:(max+1) := vinverse --type using \-1v