summaryrefslogtreecommitdiff
path: root/backends/lean
diff options
context:
space:
mode:
authorSon Ho2024-03-08 09:25:11 +0100
committerSon Ho2024-03-08 09:25:11 +0100
commit9d541d1ab6b91e59e4f78f4711af085a33ee4f82 (patch)
tree5b49f47f8851a009c3a629c18cd0e3bdc5af3c23 /backends/lean
parent41d6f78a0ad6bd272164894bead3258b2001ec0c (diff)
Update the tuples syntax
Diffstat (limited to '')
-rw-r--r--backends/lean/Base/Tuples.lean4
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