diff options
| author | Son Ho | 2024-03-08 07:56:44 +0100 |
|---|---|---|
| committer | Son Ho | 2024-03-08 07:56:44 +0100 |
| commit | bc397dea5c5a67766c9c0381efad222524f68881 (patch) | |
| tree | 81c78cede34b836daff3f1aa8f8fdc9b553b627a | |
| parent | 23ce25c77052c02312f19f17c51fe0b61d6abc93 (diff) | |
Update the notation for heterogeneous negation
| -rw-r--r-- | backends/lean/Base/Primitives/Scalar.lean | 15 |
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: |