diff options
| author | Son Ho | 2024-03-08 09:25:11 +0100 |
|---|---|---|
| committer | Son Ho | 2024-03-08 09:25:11 +0100 |
| commit | 9d541d1ab6b91e59e4f78f4711af085a33ee4f82 (patch) | |
| tree | 5b49f47f8851a009c3a629c18cd0e3bdc5af3c23 /backends/lean/Base/Tuples.lean | |
| parent | 41d6f78a0ad6bd272164894bead3258b2001ec0c (diff) | |
Update the tuples syntax
Diffstat (limited to 'backends/lean/Base/Tuples.lean')
| -rw-r--r-- | backends/lean/Base/Tuples.lean | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/backends/lean/Base/Tuples.lean b/backends/lean/Base/Tuples.lean index d8e4a843..4c59dac9 100644 --- a/backends/lean/Base/Tuples.lean +++ b/backends/lean/Base/Tuples.lean @@ -8,7 +8,9 @@ namespace Primitives ------------------------------- -- Declare new syntax `a.#i` for accessing the `i`-th term in a tuple -- The `noWs` parser is used to ensure there is no whitespace. -syntax term noWs ".#" noWs num : term +-- We use the maximum precedence to make the syntax work with function calls. +-- Ex.: `f (0, 1).#0` +syntax:max term noWs ".#" noWs num : term open Lean Meta Elab Term |