From 9d541d1ab6b91e59e4f78f4711af085a33ee4f82 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 8 Mar 2024 09:25:11 +0100
Subject: Update the tuples syntax

---
 backends/lean/Base/Tuples.lean | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'backends/lean/Base/Tuples.lean')

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
 
-- 
cgit v1.2.3