Do not parenthesize structure literals

runtimeverification · Jan 24, 2025 · a9a34dd · a9a34dd
1 parent 541f4ec
commit a9a34dd
Showing 1 changed file with 5 additions and 0 deletions.
diff --git a/pyk/src/pyk/k2lean4/k2lean4.py b/pyk/src/pyk/k2lean4/k2lean4.py
@@ -454,8 +454,13 @@ def _transform_app(self, symbol: str, sorts: tuple[Sort, ...], args: tuple[Patte
 
     def _transform_arg(self, pattern: Pattern) -> Term:
         term = self._transform_pattern(pattern)
+
         if not isinstance(pattern, App):
             return term
+
+        if pattern.symbol in self.structure_symbols:
+            return term
+
         return Term(f'({term})')
 
     def _transform_inj_app(self, sorts: tuple[Sort, ...], args: tuple[Pattern, ...]) -> Term: