From bc397dea5c5a67766c9c0381efad222524f68881 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 8 Mar 2024 07:56:44 +0100
Subject: Update the notation for heterogeneous negation

---
 backends/lean/Base/Primitives/Scalar.lean | 15 ++++++++++++---
 1 file changed, 12 insertions(+), 3 deletions(-)

(limited to 'backends/lean/Base/Primitives')

diff --git a/backends/lean/Base/Primitives/Scalar.lean b/backends/lean/Base/Primitives/Scalar.lean
index 422cbc6a..3afd13d2 100644
--- a/backends/lean/Base/Primitives/Scalar.lean
+++ b/backends/lean/Base/Primitives/Scalar.lean
@@ -478,15 +478,24 @@ instance (ty : ScalarTy) : Inhabited (Scalar ty) := by
 Remark: there is no heterogeneous negation in the Lean prelude: we thus introduce
 one here.
 
-The notation typeclass for heterogeneous addition.
-This enables the notation `- a : β` where `a : α`.
+The notation typeclass for heterogeneous negation.
 -/
 class HNeg (α : Type u) (β : outParam (Type v)) where
   /-- `- a` computes the negation of `a`.
   The meaning of this notation is type-dependent. -/
   hNeg : α → β
 
-prefix:75  "-"   => HNeg.hNeg
+/- Notation for heterogeneous negation.
+
+   We initially used the notation "-" but it conflicted with the homogeneous
+   negation too much. In particular, it made terms like `-10` ambiguous,
+   and seemingly caused to backtracking in elaboration, leading to definitions
+   like arrays of constants to take an unreasonable time to get elaborated
+   and type-checked.
+
+   TODO: PR to replace Neg with HNeg in Lean?
+ -/
+prefix:75  "-."   => HNeg.hNeg
 
 /- We need this, otherwise we break pattern matching like in:
 
-- 
cgit v1.2.3