From 17f3ac6ec261d1a08705bad3a6a48888e7c06b67 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Mon, 13 Apr 2015 15:30:59 -0400 Subject: [PATCH] fix(hott): fix binding power of 2 notations --- hott/algebra/precategory/basic.hlean | 3 ++- hott/init/path.hlean | 4 ++-- 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/hott/algebra/precategory/basic.hlean b/hott/algebra/precategory/basic.hlean index 1e67ebad0..be3110420 100644 --- a/hott/algebra/precategory/basic.hlean +++ b/hott/algebra/precategory/basic.hlean @@ -132,7 +132,8 @@ namespace category attribute Precategory.struct [instance] [priority 10000] [coercion] -- definition precategory.carrier [coercion] [reducible] := Precategory.carrier -- definition precategory.struct [instance] [coercion] [reducible] := Precategory.struct - notation g `∘⁅` C `⁆` f := @comp (Precategory.carrier C) (Precategory.struct C) _ _ _ g f + notation g `∘⁅`:60 C:0 `⁆`:0 f:60 := + @comp (Precategory.carrier C) (Precategory.struct C) _ _ _ g f -- TODO: make this left associative -- TODO: change this notation? diff --git a/hott/init/path.hlean b/hott/init/path.hlean index d1dfac72e..6b1b0ecfb 100644 --- a/hott/init/path.hlean +++ b/hott/init/path.hlean @@ -40,8 +40,8 @@ namespace eq definition inverse (p : x = y) : y = x := eq.rec (refl x) p - notation p₁ ⬝ p₂ := concat p₁ p₂ - notation p ⁻¹ := inverse p + infix ⬝ := concat + postfix ⁻¹ := inverse --a second notation for the inverse, which is not overloaded postfix [parsing-only] `⁻¹ᵖ`:std.prec.max_plus := inverse