fix Lean 4 ASTs

src/lean_dojo/data_extraction/ast/lean4/node.py

@@ -668,6 +668,21 @@ def get_ident(self) -> Optional[str]:
             return self.children[0].val
 
 
+@dataclass(frozen=True)
+class LeanBinderidentAntiquotNode4(Node4):
+    @classmethod
+    def from_data(
+        cls, node_data: Dict[str, Any], lean_file: LeanFile
+    ) -> "LeanBinderidentAntiquotNode4":
+        assert node_data["info"] == "none"
+        start, end = None, None
+        children = _parse_children(node_data, lean_file)
+        return cls(lean_file, start, end, children)
+
+    def get_ident(self) -> Optional[str]:
+        return None
+
+
 @dataclass(frozen=True)
 class StdTacticAliasAliasNode4(Node4):
     name: str
@@ -712,9 +727,9 @@ def from_data(
         assert isinstance(children[6], AtomNode4) and children[6].val == "⟩"
 
         name = []
-        assert isinstance(children[3], LeanBinderidentNode4)
+        assert type(children[3]) in (LeanBinderidentNode4, LeanBinderidentAntiquotNode4)
         name.append(children[3].get_ident())
-        assert isinstance(children[5], LeanBinderidentNode4)
+        assert type(children[5]) in (LeanBinderidentNode4, LeanBinderidentAntiquotNode4)
         name.append(children[5].get_ident())
         name = [n for n in name if n is not None]
 
@@ -1071,6 +1086,23 @@ def from_data(
         return cls(lean_file, start, end, children)
 
 
+@dataclass(frozen=True)
+class TacticTacticseq1IndentedAntiquotNode4(Node4):
+    @classmethod
+    def from_data(
+        cls, node_data: Dict[str, Any], lean_file: LeanFile
+    ) -> "TacticTacticseq1IndentedAntiquotNode4":
+        assert node_data["info"] == "none"
+        start, end = None, None
+        children = _parse_children(node_data, lean_file)
+        return cls(lean_file, start, end, children)
+
+    def get_tactic_nodes(
+        self, atomic_only: bool = False
+    ) -> Generator[Node4, None, None]:
+        return
+
+
 @dataclass(frozen=True)
 class TacticTacticseqNode4(Node4):
     @classmethod
@@ -1083,7 +1115,7 @@ def from_data(
         assert len(children) == 1 and type(children[0]) in (
             TacticTacticseq1IndentedNode4,
             TacticTacticseqbracketedNode4,
-            TacticTacticSeq1IndentedAntiquotNode4,
+            TacticTacticseq1IndentedAntiquotNode4,
         )
         return cls(lean_file, start, end, children)
 
@@ -1118,24 +1150,6 @@ def get_tactic_nodes(
                 )
 
 
-@dataclass(frozen=True)
-class TacticTacticSeq1IndentedAntiquotNode4(Node4):
-    @classmethod
-    def from_data(
-        cls, node_data: Dict[str, Any], lean_file: LeanFile
-    ) -> "TacticTacticSeq1IndentedAntiquotNode4":
-        assert node_data["info"] == "none"
-        start, end = None, None
-        children = _parse_children(node_data, lean_file)
-        assert len(children) == 1 and isinstance(children[0], NullNode4)
-        return cls(lean_file, start, end, children)
-
-    def get_tactic_nodes(
-        self, atomic_only: bool = False
-    ) -> Generator[Node4, None, None]:
-        return
-
-
 @dataclass(frozen=True)
 class TacticTacticseqbracketedNode4(Node4):
     state_before: Optional[str] = None