summaryrefslogtreecommitdiff
path: root/backends/lean/Base/Primitives
diff options
context:
space:
mode:
authorSon Ho2024-03-08 07:56:44 +0100
committerSon Ho2024-03-08 07:56:44 +0100
commitbc397dea5c5a67766c9c0381efad222524f68881 (patch)
tree81c78cede34b836daff3f1aa8f8fdc9b553b627a /backends/lean/Base/Primitives
parent23ce25c77052c02312f19f17c51fe0b61d6abc93 (diff)
Update the notation for heterogeneous negation
Diffstat (limited to 'backends/lean/Base/Primitives')
-rw-r--r--backends/lean/Base/Primitives/Scalar.lean15
1 files changed, 12 insertions, 3 deletions
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: