diff options
| -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 |