feat: Implement TacticLet, TacticExpr

pantograph/expr.py

@@ -91,10 +91,39 @@ class GoalState:
 
 @dataclass(frozen=True)
 class TacticHave:
+    """
+    The `have` tactic, equivalent to
+    ```lean
+    have {binder_name} : {branch} := ...
+    ```
+    """
+    branch: str
+    binder_name: Optional[str] = None
+@dataclass(frozen=True)
+class TacticLet:
+    """
+    The `have` tactic, equivalent to
+    ```lean
+    let {binder_name} : {branch} := ...
+    ```
+    """
     branch: str
     binder_name: Optional[str] = None
 @dataclass(frozen=True)
 class TacticCalc:
+    """
+    The `calc` tactic, equivalent to
+    ```lean
+    calc {step} := ...
+    ```
+    You can use `_` in the step.
+    """
     step: str
+@dataclass(frozen=True)
+class TacticExpr:
+    """
+    Assigns an expression to the current goal
+    """
+    expr: str
 
-Tactic = Union[str, TacticHave, TacticCalc]
+Tactic = Union[str, TacticHave, TacticLet, TacticCalc, TacticExpr]

pantograph/server.py

@@ -5,8 +5,18 @@ interface.
 import json, pexpect, unittest, os
 from typing import Union
 from pathlib import Path
-from pantograph.expr import parse_expr, Expr, Variable, Goal, GoalState, \
-    Tactic, TacticHave, TacticCalc
+from pantograph.expr import (
+    parse_expr,
+    Expr,
+    Variable,
+    Goal,
+    GoalState,
+    Tactic,
+    TacticHave,
+    TacticLet,
+    TacticCalc,
+    TacticExpr,
+)
 from pantograph.compiler import TacticInvocation
 
 def _get_proc_cwd():
@@ -145,6 +155,12 @@ class Server:
             args["have"] = tactic.branch
             if tactic.binder_name:
                 args["binderName"] = tactic.binder_name
+        elif isinstance(tactic, TacticLet):
+            args["let"] = tactic.branch
+            if tactic.binder_name:
+                args["binderName"] = tactic.binder_name
+        elif isinstance(tactic, TacticExpr):
+            args["expr"] = tactic.expr
         elif isinstance(tactic, TacticCalc):
             args["calc"] = tactic.step
         else:
@@ -339,6 +355,23 @@ class TestServer(unittest.TestCase):
                 target="1 + 1 = 2",
             ),
         ])
+    def test_let(self):
+        server = Server()
+        state0 = server.goal_start("1 + 1 = 2")
+        state1 = server.goal_tactic(
+            state0, goal_id=0,
+            tactic=TacticLet(branch="2 = 1 + 1", binder_name="h"))
+        self.assertEqual(state1.goals, [
+            Goal(
+                variables=[],
+                name="h",
+                target="2 = 1 + 1",
+            ),
+            Goal(
+                variables=[Variable(name="h", t="2 = 1 + 1", v="?h")],
+                target="1 + 1 = 2",
+            ),
+        ])
 
     def test_conv_calc(self):
         server = Server(options={"automaticMode": False})

src

@@ -1 +1 @@
-Subproject commit e0ba65a7cdac889836c8f9602117668d15dc26c9
+Subproject commit 645d9c9250bf306bdf13d085a222ce03de8aa836