diff --git a/.scalafmt.conf b/.scalafmt.conf
index 3e5cd95..1899ebf 100644
--- a/.scalafmt.conf
+++ b/.scalafmt.conf
@@ -4,5 +4,3 @@ runner.dialect = scala3
 assumeStandardLibraryStripMargin = true
 align.stripMargin = true
 rewrite.trailingCommas.style = "always"
-
-comments.wrap = "standalone"
diff --git a/langs/tla/ExprMarker.scala b/langs/tla/ExprMarker.scala
new file mode 100644
index 0000000..f8e090e
--- /dev/null
+++ b/langs/tla/ExprMarker.scala
@@ -0,0 +1,371 @@
+// Copyright 2024-2025 Forja Team
+//
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//     http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+package forja.langs.tla
+
+import cats.syntax.all.given
+
+import forja.*
+import forja.dsl.*
+import forja.wf.Wellformed
+
+import TLAReader.*
+
+object ExprMarker extends PassSeq:
+
+  lazy val passes = List(
+    buildExpressions,
+    // removeNestedExpr
+  )
+
+  object ExprTry extends Token
+  def inputWellformed: Wellformed = TLAParser.outputWellformed
+
+  def parsedChildrenSepBy(
+      parent: Token,
+      split: SeqPattern[?],
+  ): SeqPattern[List[Node]] =
+    leftSibling(ExprTry) *>
+      tok(parent) *>
+      children:
+        field(
+          repeatedSepBy(split)(
+            skip(ExprTry)
+              ~ field(lang.Expr)
+              ~ trailing,
+          ),
+        )
+          ~ eof
+  end parsedChildrenSepBy
+
+  // TODO: I wonder if this pattern is a bad idea
+  def firstUnmarkedChildStart(
+      paren: Token,
+  ): SeqPattern[Node] =
+    parent(leftSibling(ExprTry) *> paren) *>
+      not(leftSibling(anyNode)) *>
+      not(ExprTry) *> not(lang.Expr) *> anyNode
+  end firstUnmarkedChildStart
+
+  def unMarkedChildSplit(
+      paren: Token,
+      split: Token,
+  ): SeqPattern[Node] =
+    parent(leftSibling(ExprTry) *> paren) *>
+      possibleExprTryToRight(split)
+  end unMarkedChildSplit
+
+  def rightSiblingNotExprTry(): SeqPattern[Unit] =
+    rightSibling(not(lang.Expr) *> not(ExprTry))
+  end rightSiblingNotExprTry
+
+  def possibleExprTryToRight(
+      node: SeqPattern[Node],
+  ): SeqPattern[Node] =
+    node <* rightSiblingNotExprTry()
+  end possibleExprTryToRight
+
+  object buildExpressions extends Pass:
+    val wellformed = prevWellformed.makeDerived:
+      val removedCases = Seq(
+        TLAReader.StringLiteral,
+        TLAReader.NumberLiteral,
+        TLAReader.TupleGroup,
+        // TODO: remove cases
+      )
+      TLAReader.groupTokens.foreach: tok =>
+        tok.removeCases(removedCases*)
+        tok.addCases(lang.Expr)
+
+      lang.Expr.deleteShape()
+      lang.Expr.importFrom(lang.wf)
+      lang.Expr.addCases(lang.Expr)
+
+    val rules =
+      pass(once = false, strategy = pass.bottomUp)
+        .rules:
+          // Parse Number and String Literals
+          on(
+            leftSibling(ExprTry) *>
+              field(TLAReader.NumberLiteral)
+              ~ trailing,
+          ).rewrite: lit =>
+            splice(lang.Expr(lang.Expr.NumberLiteral().like(lit)))
+          | on(
+            leftSibling(ExprTry) *>
+              field(TLAReader.StringLiteral)
+              ~ trailing,
+          ).rewrite: lit =>
+            splice(lang.Expr(lang.Expr.StringLiteral().like(lit)))
+          // Parse Id
+          | on(
+            leftSibling(ExprTry) *>
+              field(TLAReader.Alpha)
+              ~ trailing,
+          ).rewrite: id =>
+            splice(
+              lang.Expr(
+                lang.Expr.OpCall(
+                  lang.Id().like(id.unparent()),
+                  lang.Expr.OpCall.Params(),
+                ),
+              ),
+            )
+          // TupleLiteral is complete when all the elements are parsed
+          | on(
+            parsedChildrenSepBy(TLAReader.TupleGroup, `,`),
+          ).rewrite: exprs =>
+            splice(
+              lang.Expr(
+                lang.Expr.TupleLiteral(exprs.iterator.map(_.unparent())),
+              ),
+            )
+          // If the TupleLiteral not complete, mark the elements with ExprTry
+          // Mark the first child in the first pass, and then mark the rest in
+          // the second
+          | on(
+            firstUnmarkedChildStart(TLAReader.TupleGroup),
+          ).rewrite: first =>
+            splice(ExprTry(), first.unparent())
+          | on(
+            unMarkedChildSplit(TLAReader.TupleGroup, `,`),
+          ).rewrite: split =>
+            splice(split.unparent(), ExprTry())
+          // SetLiteral is complete when all the elements are parsed
+          | on(
+            parsedChildrenSepBy(TLAReader.BracesGroup, `,`),
+          ).rewrite: exprs =>
+            splice(
+              lang.Expr(
+                lang.Expr.SetLiteral(exprs.iterator.map(_.unparent())),
+              ),
+            )
+          // If the SetLiteral is not complete, mark the elements with ExprTry
+          // Mark the first child in the first pass, and then mark the rest in
+          // the second
+          | on(
+            firstUnmarkedChildStart(TLAReader.BracesGroup),
+          ).rewrite: first =>
+            splice(ExprTry(), first.unparent())
+          | on(
+            unMarkedChildSplit(TLAReader.BracesGroup, `,`),
+          ).rewrite: split =>
+            splice(split.unparent(), ExprTry())
+          // RecordLiteral is complete when all the elements are parsed
+          | on(
+            leftSibling(ExprTry) *> tok(TLAReader.SqBracketsGroup) *>
+              children:
+                field(
+                  repeatedSepBy1(`,`)(
+                    field(TLAReader.Alpha)
+                      ~ skip(TLAReader.`|->`)
+                      ~ skip(ExprTry)
+                      ~ field(lang.Expr)
+                      ~ trailing,
+                  ),
+                )
+                  ~ eof,
+          ).rewrite: records =>
+            splice(
+              lang.Expr(
+                lang.Expr.RecordLiteral(
+                  records.iterator.map((id, expr) =>
+                    lang.Expr.RecordLiteral.Field(
+                      lang.Id().like(id.unparent()),
+                      expr.unparent(),
+                    ),
+                  ),
+                ),
+              ),
+            )
+          // If the RecordLiteral is not complete, place ExprTry after each |->
+          | on(
+            unMarkedChildSplit(TLAReader.SqBracketsGroup, `|->`),
+          ).rewrite: split =>
+            splice(split.unparent(), ExprTry())
+          // Parse Projection (Record field access)
+          | on(
+            leftSibling(ExprTry) *>
+              field(lang.Expr)
+              ~ skip(defns.`.`)
+              ~ field(TLAReader.Alpha)
+              ~ trailing,
+          ).rewrite: (expr, id) =>
+            splice(
+              lang.Expr(
+                lang.Expr.Project(
+                  expr.unparent(),
+                  lang.Id().like(id.unparent()),
+                ),
+              ),
+            )
+          // IF is complete when every branch is parsed.
+          | on(
+            leftSibling(ExprTry) *>
+              skip(defns.IF)
+              ~ skip(ExprTry)
+              ~ field(lang.Expr)
+              ~ skip(defns.THEN)
+              ~ skip(ExprTry)
+              ~ field(lang.Expr)
+              ~ skip(defns.ELSE)
+              ~ skip(ExprTry)
+              ~ field(lang.Expr)
+              ~ trailing,
+          ).rewrite: (pred, t, f) =>
+            splice(
+              lang.Expr(
+                lang.Expr.If(
+                  pred.unparent(),
+                  t.unparent(),
+                  f.unparent(),
+                ),
+              ),
+            )
+          // If IF is not complete, place ExprTry before the pred and branches
+          | on(
+            possibleExprTryToRight(
+              tok(defns.IF) | tok(defns.THEN) | tok(defns.ELSE),
+            ),
+          ).rewrite: split =>
+            splice(split.unparent(), ExprTry())
+          // CASE is complete when every branch is parsed.
+          | on(
+            leftSibling(ExprTry) *>
+              skip(defns.CASE)
+              ~ field(
+                repeatedSepBy1(defns.`[]`)(
+                  skip(ExprTry)
+                    ~ field(lang.Expr)
+                    ~ skip(TLAReader.`->`)
+                    ~ skip(ExprTry)
+                    ~ field(lang.Expr)
+                    ~ trailing,
+                ),
+              )
+              ~ field(
+                optional(
+                  skip(defns.OTHER)
+                    ~ skip(TLAReader.`->`)
+                    ~ skip(ExprTry)
+                    ~ field(lang.Expr)
+                    ~ eof,
+                ),
+              )
+              ~ trailing,
+          ).rewrite: (cases, other) =>
+            splice(
+              lang.Expr(
+                lang.Expr.Case(
+                  lang.Expr.Case.Branches(
+                    cases.iterator.map((pred, branch) =>
+                      lang.Expr.Case.Branch(pred.unparent(), branch.unparent()),
+                    ),
+                  ),
+                  lang.Expr.Case.Other(
+                    other match
+                      case None       => lang.Expr.Case.None()
+                      case Some(expr) => expr.unparent(),
+                  ),
+                ),
+              ),
+            )
+          // If the CASE is not complete, insert ExprTry after [], ->, and OTHER
+          //  as well as before the first case.
+          | on(
+            possibleExprTryToRight(leftSibling(ExprTry) *> defns.CASE),
+          ).rewrite: c =>
+            splice(c.unparent(), ExprTry())
+          | on(
+            possibleExprTryToRight((tok(defns.`[]`) | tok(TLAReader.`->`))),
+          ).rewrite: split =>
+            splice(split.unparent(), ExprTry())
+          | on(
+            possibleExprTryToRight(
+              leftSibling(defns.OTHER) *> tok(TLAReader.`->`),
+            ),
+          ).rewrite: split =>
+            splice(split.unparent(), ExprTry())
+          // LET is complete when the definitions and the body are parsed
+          // I am assuming TLAParser will have inserted an ExpTry before the let
+          // body
+          | on(
+            leftSibling(ExprTry) *>
+              field(
+                tok(TLAReader.LetGroup) *>
+                  children(
+                    repeated:
+                      tok(lang.Operator)
+                        | tok(lang.ModuleDefinition)
+                        | tok(lang.Recursive),
+                  ),
+              )
+              ~ skip(ExprTry)
+              ~ field(lang.Expr)
+              ~ trailing,
+          ).rewrite: (defs, body) =>
+            splice(
+              lang.Expr(
+                lang.Expr.Let(
+                  lang.Expr.Let.Defns(
+                    defs.iterator.map(_.unparent()),
+                  ),
+                  body.unparent(),
+                ),
+              ),
+            )
+          // Parentheses can be removed when its children are parsed
+          | on(
+            leftSibling(ExprTry) *>
+              tok(TLAReader.ParenthesesGroup) *>
+              children(
+                skip(ExprTry)
+                  ~ field(lang.Expr)
+                  ~ eof,
+              ),
+          ).rewrite: expr =>
+            splice(expr.unparent())
+          // Mark the children of the parentheses
+          | on(
+            firstUnmarkedChildStart(TLAReader.ParenthesesGroup),
+          ).rewrite: node =>
+            splice(ExprTry(), node.unparent())
+      *> pass(once = false, strategy = pass.bottomUp)
+        .rules:
+          // Expr has been parsed sucessfully, and ExprTry can be removed
+          // I have to do it this way, otherwise ExprTry might get removed too
+          // early.
+          on(
+            skip(ExprTry)
+              ~ field(lang.Expr)
+              ~ eof,
+          ).rewrite: expr =>
+            splice(expr.unparent())
+  end buildExpressions
+
+  object removeNestedExpr extends Pass:
+    val wellformed = prevWellformed.makeDerived:
+      lang.Expr.removeCases(lang.Expr)
+
+    val rules =
+      pass(once = true, strategy = pass.bottomUp)
+        .rules:
+          on(
+            tok(lang.Expr) *>
+              onlyChild(lang.Expr),
+          ).rewrite: child =>
+            splice(
+              child.unparent(),
+            )
+  end removeNestedExpr
diff --git a/langs/tla/ExprMarker.test.scala b/langs/tla/ExprMarker.test.scala
new file mode 100644
index 0000000..bf4f271
--- /dev/null
+++ b/langs/tla/ExprMarker.test.scala
@@ -0,0 +1,456 @@
+// Copyright 2024-2025 Forja Team
+//
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//     http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+package forja.langs.tla
+
+import forja.*
+import forja.dsl.*
+
+import ExprMarker.ExprTry
+
+// Run with:
+// scala-cli test . -- '*ExprMarker*'
+
+class ExprMarkerTests extends munit.FunSuite:
+  extension (top: Node.Top)
+    def parseNode: Node.Top =
+      val freshTop = Node.Top(
+        lang.Module(
+          lang.Id("TestMod"),
+          lang.Module.Extends(),
+          lang.Module.Defns(
+            lang.Operator(
+              lang.Id("test"),
+              lang.Operator.Params(),
+              lang.Expr(
+                top.unparentedChildren,
+              ),
+            ),
+          ),
+        ),
+      )
+      /* instrumentWithTracer(forja.manip.RewriteDebugTracer(os.pwd /
+       * "dbg_exprmarker")): */
+      ExprMarker(freshTop)
+      Node.Top(
+        freshTop(lang.Module)(lang.Module.Defns)(lang.Operator)(
+          lang.Expr,
+        ).unparentedChildren,
+      )
+
+  test("NumberLiteral"):
+    assertEquals(
+      Node.Top(ExprTry(), TLAReader.NumberLiteral("1")).parseNode,
+      Node.Top(lang.Expr(lang.Expr.NumberLiteral("1"))),
+    )
+
+  test("StringLiteral"):
+    assertEquals(
+      Node.Top(ExprTry(), TLAReader.StringLiteral("string")).parseNode,
+      Node.Top(lang.Expr(lang.Expr.StringLiteral("string"))),
+    )
+
+  test("Id"):
+    assertEquals(
+      Node.Top(ExprTry(), TLAReader.Alpha("X")).parseNode,
+      Node.Top(
+        lang.Expr(
+          lang.Expr.OpCall(
+            lang.Id("X"),
+            lang.Expr.OpCall.Params(),
+          ),
+        ),
+      ),
+    )
+
+  test("ParenthesesGroup"):
+    assertEquals(
+      Node
+        .Top(
+          ExprTry(),
+          TLAReader.ParenthesesGroup(
+            TLAReader.NumberLiteral("1"),
+          ),
+        )
+        .parseNode,
+      Node.Top(lang.Expr(lang.Expr.NumberLiteral("1"))),
+    )
+    // TODO: paranthesis with op
+
+  test("SetLiteral"):
+    // empty set
+    assertEquals(
+      Node.Top(ExprTry(), TLAReader.BracesGroup()).parseNode,
+      Node.Top(lang.Expr(lang.Expr.SetLiteral())),
+    )
+    // set with three elements
+    assertEquals(
+      Node
+        .Top(
+          ExprTry(),
+          TLAReader.BracesGroup(
+            TLAReader.NumberLiteral("1"),
+            TLAReader.`,`(","),
+            TLAReader.NumberLiteral("2"),
+            TLAReader.`,`(","),
+            TLAReader.NumberLiteral("3"),
+          ),
+        )
+        .parseNode,
+      Node.Top(
+        lang.Expr(
+          lang.Expr.SetLiteral(
+            lang.Expr(lang.Expr.NumberLiteral("1")),
+            lang.Expr(lang.Expr.NumberLiteral("2")),
+            lang.Expr(lang.Expr.NumberLiteral("3")),
+          ),
+        ),
+      ),
+    )
+    // nested sets
+    assertEquals(
+      Node
+        .Top(
+          ExprTry(),
+          TLAReader.BracesGroup(
+            TLAReader.NumberLiteral("1"),
+            TLAReader.`,`(","),
+            TLAReader.BracesGroup(),
+            TLAReader.`,`(","),
+            TLAReader.NumberLiteral("3"),
+          ),
+        )
+        .parseNode,
+      Node.Top(
+        lang.Expr(
+          lang.Expr.SetLiteral(
+            lang.Expr(lang.Expr.NumberLiteral("1")),
+            lang.Expr(lang.Expr.SetLiteral()),
+            lang.Expr(lang.Expr.NumberLiteral("3")),
+          ),
+        ),
+      ),
+    )
+
+  test("TupleLiteral"):
+    // empty tuple
+    assertEquals(
+      Node.Top(ExprTry(), TLAReader.TupleGroup()).parseNode,
+      Node.Top(lang.Expr(lang.Expr.TupleLiteral())),
+    )
+    // tuple with three elements
+    assertEquals(
+      Node
+        .Top(
+          ExprTry(),
+          TLAReader.TupleGroup(
+            TLAReader.NumberLiteral("1"),
+            TLAReader.`,`(","),
+            TLAReader.StringLiteral("two"),
+            TLAReader.`,`(","),
+            TLAReader.NumberLiteral("3"),
+          ),
+        )
+        .parseNode,
+      Node.Top(
+        lang.Expr(
+          lang.Expr.TupleLiteral(
+            lang.Expr(lang.Expr.NumberLiteral("1")),
+            lang.Expr(lang.Expr.StringLiteral("two")),
+            lang.Expr(lang.Expr.NumberLiteral("3")),
+          ),
+        ),
+      ),
+    )
+
+  test("RecordLiteral"):
+    // record with three fields
+    assertEquals(
+      Node
+        .Top(
+          ExprTry(),
+          TLAReader.SqBracketsGroup(
+            TLAReader.Alpha("X"),
+            TLAReader.`|->`("|->"),
+            TLAReader.NumberLiteral("1"),
+            TLAReader.`,`(","),
+            TLAReader.Alpha("Y"),
+            TLAReader.`|->`("|->"),
+            TLAReader.NumberLiteral("2"),
+            TLAReader.`,`(","),
+            TLAReader.Alpha("Z"),
+            TLAReader.`|->`("|->"),
+            TLAReader.NumberLiteral("3"),
+          ),
+        )
+        .parseNode,
+      Node.Top(
+        lang.Expr(
+          lang.Expr.RecordLiteral(
+            lang.Expr.RecordLiteral.Field(
+              lang.Id("X"),
+              lang.Expr(lang.Expr.NumberLiteral("1")),
+            ),
+            lang.Expr.RecordLiteral.Field(
+              lang.Id("Y"),
+              lang.Expr(lang.Expr.NumberLiteral("2")),
+            ),
+            lang.Expr.RecordLiteral.Field(
+              lang.Id("Z"),
+              lang.Expr(lang.Expr.NumberLiteral("3")),
+            ),
+          ),
+        ),
+      ),
+    )
+
+  test("Projection (Record Field Acess)"):
+    assertEquals(
+      Node
+        .Top(
+          ExprTry(),
+          TLAReader.Alpha("X"),
+          defns.`.`("."),
+          TLAReader.Alpha("Y"),
+        )
+        .parseNode,
+      Node.Top(
+        lang.Expr(
+          lang.Expr.Project(
+            lang.Expr(
+              lang.Expr.OpCall(
+                lang.Id("X"),
+                lang.Expr.OpCall.Params(),
+              ),
+            ),
+            lang.Id("Y"),
+          ),
+        ),
+      ),
+    )
+    assertEquals(
+      Node
+        .Top(
+          ExprTry(),
+          TLAReader.Alpha("X"),
+          defns.`.`("."),
+          TLAReader.Alpha("Y"),
+          defns.`.`("."),
+          TLAReader.Alpha("Z"),
+        )
+        .parseNode,
+      Node.Top(
+        lang.Expr(
+          lang.Expr.Project(
+            lang.Expr(
+              lang.Expr.Project(
+                lang.Expr(
+                  lang.Expr.OpCall(
+                    lang.Id("X"),
+                    lang.Expr.OpCall.Params(),
+                  ),
+                ),
+                lang.Id("Y"),
+              ),
+            ),
+            lang.Id("Z"),
+          ),
+        ),
+      ),
+    )
+
+  test("If"):
+    assertEquals(
+      Node
+        .Top(
+          ExprTry(),
+          defns.IF(),
+          TLAReader.Alpha("A"),
+          defns.THEN(),
+          TLAReader.NumberLiteral("1"),
+          defns.ELSE(),
+          TLAReader.NumberLiteral("2"),
+        )
+        .parseNode,
+      Node.Top(
+        lang.Expr(
+          lang.Expr.If(
+            lang.Expr(
+              lang.Expr.OpCall(
+                lang.Id("A"),
+                lang.Expr.OpCall.Params(),
+              ),
+            ),
+            lang.Expr(lang.Expr.NumberLiteral("1")),
+            lang.Expr(lang.Expr.NumberLiteral("2")),
+          ),
+        ),
+      ),
+    )
+
+  test("Case"):
+    assertEquals(
+      Node
+        .Top(
+          ExprTry(),
+          defns.CASE(),
+          TLAReader.StringLiteral("A"),
+          TLAReader.`->`("->"),
+          TLAReader.NumberLiteral("1"),
+        )
+        .parseNode,
+      Node.Top(
+        lang.Expr(
+          lang.Expr.Case(
+            lang.Expr.Case.Branches(
+              lang.Expr.Case.Branch(
+                lang.Expr(lang.Expr.StringLiteral("A")),
+                lang.Expr(lang.Expr.NumberLiteral("1")),
+              ),
+            ),
+            lang.Expr.Case.Other(lang.Expr.Case.None()),
+          ),
+        ),
+      ),
+    )
+    assertEquals(
+      Node
+        .Top(
+          ExprTry(),
+          defns.CASE(),
+          TLAReader.StringLiteral("A"),
+          TLAReader.`->`("->"),
+          TLAReader.NumberLiteral("1"),
+          defns.`[]`("[]"),
+          TLAReader.StringLiteral("B"),
+          TLAReader.`->`("->"),
+          TLAReader.NumberLiteral("2"),
+        )
+        .parseNode,
+      Node.Top(
+        lang.Expr(
+          lang.Expr.Case(
+            lang.Expr.Case.Branches(
+              lang.Expr.Case.Branch(
+                lang.Expr(lang.Expr.StringLiteral("A")),
+                lang.Expr(lang.Expr.NumberLiteral("1")),
+              ),
+              lang.Expr.Case.Branch(
+                lang.Expr(lang.Expr.StringLiteral("B")),
+                lang.Expr(lang.Expr.NumberLiteral("2")),
+              ),
+            ),
+            lang.Expr.Case.Other(lang.Expr.Case.None()),
+          ),
+        ),
+      ),
+    )
+    assertEquals(
+      Node
+        .Top(
+          ExprTry(),
+          defns.CASE(),
+          TLAReader.StringLiteral("A"),
+          TLAReader.`->`("->"),
+          TLAReader.NumberLiteral("1"),
+          defns.`[]`("[]"),
+          TLAReader.StringLiteral("B"),
+          TLAReader.`->`("->"),
+          TLAReader.NumberLiteral("2"),
+          defns.OTHER("OTHER"),
+          TLAReader.`->`("->"),
+          TLAReader.NumberLiteral("3"),
+        )
+        .parseNode,
+      Node.Top(
+        lang.Expr(
+          lang.Expr.Case(
+            lang.Expr.Case.Branches(
+              lang.Expr.Case.Branch(
+                lang.Expr(lang.Expr.StringLiteral("A")),
+                lang.Expr(lang.Expr.NumberLiteral("1")),
+              ),
+              lang.Expr.Case.Branch(
+                lang.Expr(lang.Expr.StringLiteral("B")),
+                lang.Expr(lang.Expr.NumberLiteral("2")),
+              ),
+            ),
+            lang.Expr.Case.Other(lang.Expr(lang.Expr.NumberLiteral("3"))),
+          ),
+        ),
+      ),
+    )
+
+  /* This test assumes that TLAParser has parsed the definitions and has
+   * inserted the ExprTry before the let body. */
+  /* TODO: I am not sure what kind of node I should pass to lang.Operator. It
+   * complains if it is an Expr. */
+  // test("LET"):
+  //   assertEquals(
+  //     Node.Top(
+  //       ExprTry(),
+  //       TLAReader.LetGroup(
+  //         lang.Operator(
+  //           lang.Id("X"),
+  //           lang.Operator.Params(),
+  //           lang.Expr(lang.Expr.NumberLiteral("1")),
+  //         ),
+  //         lang.Operator(
+  //           lang.Id("Y"),
+  //           lang.Operator.Params(),
+  //           lang.Expr(lang.Expr.NumberLiteral("2")),
+  //         ),
+  //       ),
+  //       ExprTry(),
+  //       TLAReader.BracesGroup(
+  //         TLAReader.Alpha("X"),
+  //         TLAReader.`,`(","),
+  //         TLAReader.Alpha("Y"),
+  //       )
+  //     ).parseNode,
+  //     Node.Top(
+  //       lang.Expr(
+  //         lang.Expr.Let(
+  //           lang.Expr.Let.Defns(
+  //             lang.Operator(
+  //               lang.Id("X"),
+  //               lang.Operator.Params(),
+  //               lang.Expr(lang.Expr.NumberLiteral("1")),
+  //             ),
+  //             lang.Operator(
+  //               lang.Id("Y"),
+  //               lang.Operator.Params(),
+  //               lang.Expr(lang.Expr.NumberLiteral("2")),
+  //             ),
+  //           ),
+  //           lang.Expr(
+  //             lang.Expr.SetLiteral(
+  //               lang.Expr(
+  //                 lang.Expr.OpCall(
+  //                   lang.Id("Y"),
+  //                   lang.Expr.OpCall.Params(),
+  //                 ),
+  //               ),
+  //               lang.Expr(
+  //                 lang.Expr.OpCall(
+  //                   lang.Id("X"),
+  //                   lang.Expr.OpCall.Params(),
+  //                 ),
+  //               ),
+  //             ),
+  //           ),
+  //         ),
+  //       ),
+  //     )
+  //   )
diff --git a/langs/tla/TLAReader.scala b/langs/tla/TLAReader.scala
index 91d955d..8affd1e 100644
--- a/langs/tla/TLAReader.scala
+++ b/langs/tla/TLAReader.scala
@@ -18,6 +18,7 @@ import cats.syntax.all.given
 
 import forja.*
 import forja.dsl.*
+import forja.langs.tla.ExprMarker.ExprTry
 import forja.source.{Reader, SourceRange}
 import forja.wf.Wellformed
 
@@ -54,6 +55,8 @@ object TLAReader extends Reader:
         Comment,
         DashSeq,
         EqSeq,
+        //
+        ExprTry,
       )
         | choice(NonAlpha.instances.toSet)
         | choice(allOperators.toSet)
@@ -70,6 +73,7 @@ object TLAReader extends Reader:
     NumberLiteral ::= Atom
     Alpha ::= Atom
     LaTexLike ::= Atom
+    ExprTry ::= Atom
 
     StepMarker ::= fields(
       choice(StepMarker.Num, StepMarker.Plus, StepMarker.Star),
@@ -120,6 +124,7 @@ object TLAReader extends Reader:
   case object `:` extends NonAlpha
   case object `::` extends NonAlpha
   case object `<-` extends NonAlpha
+  case object `->` extends NonAlpha
   case object `|->` extends NonAlpha
   case object `,` extends NonAlpha
   case object `.` extends NonAlpha
diff --git a/langs/tla/package.scala b/langs/tla/package.scala
index 2bfee44..232cfea 100644
--- a/langs/tla/package.scala
+++ b/langs/tla/package.scala
@@ -100,8 +100,8 @@ object lang extends WellformedDef:
           Expr.SetLiteral,
           Expr.TupleLiteral,
           Expr.RecordLiteral,
-          Expr.Project,
           Expr.RecordSetLiteral,
+          Expr.Project,
           Expr.OpCall,
           Expr.FnCall,
           Expr.If,
diff --git a/project.scala b/project.scala
index 0a77987..ee80bbe 100644
--- a/project.scala
+++ b/project.scala
@@ -5,9 +5,9 @@
 
 //> using dependency com.github.scopt::scopt:4.1.0
 //> using dependency com.lihaoyi::os-lib:0.11.5
-//> using dependency com.lihaoyi::pprint:0.9.3
+//> using dependency com.lihaoyi::pprint:0.9.4
 //> using dependency com.lihaoyi::sourcecode:0.4.4
-//> using dependency com.lihaoyi::ujson::4.3.0
+//> using dependency com.lihaoyi::ujson::4.4.0
 //> using dependency dev.zio::izumi-reflect:3.0.6
 //> using dependency edu.berkeley.cs.jqf:jqf-fuzz:2.1
 //> using dependency edu.berkeley.cs.jqf:jqf-instrument:2.1
@@ -15,4 +15,4 @@
 //> using dependency org.typelevel::cats-core:2.13.0
 
 // Test
-//> using test.dependency org.scalameta::munit:1.1.1
+//> using test.dependency org.scalameta::munit:1.2.1