lean_dojo.data_extraction.ast

lean_dojo.data_extraction.ast

class lean_dojo.data_extraction.ast.AtomNode(lean_file: lean_dojo.data_extraction.lean.LeanFile, start: lean_dojo.data_extraction.lean.Pos | None, end: lean_dojo.data_extraction.lean.Pos | None, children: List[ForwardRef('Node')], leading: str, trailing: str, val: str)

Bases: Node

classmethod from_data(atom_data: Dict[str, Any], lean_file: LeanFile) → AtomNode | None

leading: str

trailing: str

val: str

class lean_dojo.data_extraction.ast.CommandAbbrevNode(lean_file: lean_dojo.data_extraction.lean.LeanFile, start: lean_dojo.data_extraction.lean.Pos | None, end: lean_dojo.data_extraction.lean.Pos | None, children: List[ForwardRef('Node')], name: str)

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) → CommandAbbrevNode

name: str

class lean_dojo.data_extraction.ast.CommandAxiomNode(lean_file: lean_dojo.data_extraction.lean.LeanFile, start: lean_dojo.data_extraction.lean.Pos | None, end: lean_dojo.data_extraction.lean.Pos | None, children: List[ForwardRef('Node')], name: str)

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) → CommandAxiomNode

name: str

class lean_dojo.data_extraction.ast.CommandClassinductiveNode(lean_file: lean_dojo.data_extraction.lean.LeanFile, start: lean_dojo.data_extraction.lean.Pos | None, end: lean_dojo.data_extraction.lean.Pos | None, children: List[ForwardRef('Node')], name: str)

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) → CommandClassinductiveNode

name: str

class lean_dojo.data_extraction.ast.CommandClasstkNode(lean_file: lean_dojo.data_extraction.lean.LeanFile, start: lean_dojo.data_extraction.lean.Pos | None, end: lean_dojo.data_extraction.lean.Pos | None, children: List[ForwardRef('Node')])

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) → CommandClasstkNode

class lean_dojo.data_extraction.ast.CommandDeclarationNode(lean_file: lean_dojo.data_extraction.lean.LeanFile, start: lean_dojo.data_extraction.lean.Pos | None, end: lean_dojo.data_extraction.lean.Pos | None, children: List[ForwardRef('Node')], name: str, full_name: str | None = None)

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) → CommandDeclarationNode

full_name: str | None = None

get_theorem_node() → CommandTheoremNode

property is_example: bool

property is_theorem: bool

name: str

class lean_dojo.data_extraction.ast.CommandDeclidAntiquotNode(lean_file: lean_dojo.data_extraction.lean.LeanFile, start: lean_dojo.data_extraction.lean.Pos | None, end: lean_dojo.data_extraction.lean.Pos | None, children: List[ForwardRef('Node')])

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) → CommandDeclidAntiquotNode

class lean_dojo.data_extraction.ast.CommandDeclidNode(lean_file: lean_dojo.data_extraction.lean.LeanFile, start: lean_dojo.data_extraction.lean.Pos | None, end: lean_dojo.data_extraction.lean.Pos | None, children: List[ForwardRef('Node')])

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) → CommandDeclidNode

class lean_dojo.data_extraction.ast.CommandDeclmodifiersAntiquotNode(lean_file: lean_dojo.data_extraction.lean.LeanFile, start: lean_dojo.data_extraction.lean.Pos | None, end: lean_dojo.data_extraction.lean.Pos | None, children: List[ForwardRef('Node')])

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) → CommandDeclmodifiersAntiquotNode

class lean_dojo.data_extraction.ast.CommandDeclmodifiersNode(lean_file: lean_dojo.data_extraction.lean.LeanFile, start: lean_dojo.data_extraction.lean.Pos | None, end: lean_dojo.data_extraction.lean.Pos | None, children: List[ForwardRef('Node')])

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) → CommandDeclmodifiersNode

is_private() → bool

class lean_dojo.data_extraction.ast.CommandDeclsigNode(lean_file: lean_dojo.data_extraction.lean.LeanFile, start: lean_dojo.data_extraction.lean.Pos | None, end: lean_dojo.data_extraction.lean.Pos | None, children: List[ForwardRef('Node')])

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) → CommandDeclsigNode

class lean_dojo.data_extraction.ast.CommandDeclvaleqnsNode(lean_file: lean_dojo.data_extraction.lean.LeanFile, start: lean_dojo.data_extraction.lean.Pos | None, end: lean_dojo.data_extraction.lean.Pos | None, children: List[ForwardRef('Node')])

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) → CommandDeclvaleqnsNode

class lean_dojo.data_extraction.ast.CommandDeclvalsimpleNode(lean_file: lean_dojo.data_extraction.lean.LeanFile, start: lean_dojo.data_extraction.lean.Pos | None, end: lean_dojo.data_extraction.lean.Pos | None, children: List[ForwardRef('Node')])

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) → CommandDeclvalsimpleNode

class lean_dojo.data_extraction.ast.CommandDefNode(lean_file: lean_dojo.data_extraction.lean.LeanFile, start: lean_dojo.data_extraction.lean.Pos | None, end: lean_dojo.data_extraction.lean.Pos | None, children: List[ForwardRef('Node')], name: str)

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) → CommandDefNode

name: str

class lean_dojo.data_extraction.ast.CommandDefinitionNode(lean_file: lean_dojo.data_extraction.lean.LeanFile, start: lean_dojo.data_extraction.lean.Pos | None, end: lean_dojo.data_extraction.lean.Pos | None, children: List[ForwardRef('Node')], name: str)

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) → CommandDefinitionNode

name: str

class lean_dojo.data_extraction.ast.CommandDoccommentNode(lean_file: lean_dojo.data_extraction.lean.LeanFile, start: lean_dojo.data_extraction.lean.Pos | None, end: lean_dojo.data_extraction.lean.Pos | None, children: List[ForwardRef('Node')], comment: str)

Bases: Node

comment: str

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) → CommandDoccommentNode

class lean_dojo.data_extraction.ast.CommandEndNode(lean_file: lean_dojo.data_extraction.lean.LeanFile, start: lean_dojo.data_extraction.lean.Pos | None, end: lean_dojo.data_extraction.lean.Pos | None, children: List[ForwardRef('Node')], name: str | None)

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) → CommandEndNode

name: str | None

class lean_dojo.data_extraction.ast.CommandExampleNode(lean_file: lean_dojo.data_extraction.lean.LeanFile, start: lean_dojo.data_extraction.lean.Pos | None, end: lean_dojo.data_extraction.lean.Pos | None, children: List[ForwardRef('Node')], name: str)

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) → CommandExampleNode

name: str

class lean_dojo.data_extraction.ast.CommandInductiveNode(lean_file: lean_dojo.data_extraction.lean.LeanFile, start: lean_dojo.data_extraction.lean.Pos | None, end: lean_dojo.data_extraction.lean.Pos | None, children: List[ForwardRef('Node')], name: str | None)

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) → CommandInductiveNode

name: str | None

class lean_dojo.data_extraction.ast.CommandInstanceNode(lean_file: lean_dojo.data_extraction.lean.LeanFile, start: lean_dojo.data_extraction.lean.Pos | None, end: lean_dojo.data_extraction.lean.Pos | None, children: List[ForwardRef('Node')], name: str)

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) → CommandInstanceNode

name: str

class lean_dojo.data_extraction.ast.CommandModuledocNode(lean_file: lean_dojo.data_extraction.lean.LeanFile, start: lean_dojo.data_extraction.lean.Pos | None, end: lean_dojo.data_extraction.lean.Pos | None, children: List[ForwardRef('Node')], comment: str)

Bases: Node

comment: str

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) → CommandModuledocNode

class lean_dojo.data_extraction.ast.CommandNamespaceNode(lean_file: lean_dojo.data_extraction.lean.LeanFile, start: lean_dojo.data_extraction.lean.Pos | None, end: lean_dojo.data_extraction.lean.Pos | None, children: List[ForwardRef('Node')], name: str)

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) → CommandNamespaceNode

name: str

class lean_dojo.data_extraction.ast.CommandNoncomputablesectionNode(lean_file: lean_dojo.data_extraction.lean.LeanFile, start: lean_dojo.data_extraction.lean.Pos | None, end: lean_dojo.data_extraction.lean.Pos | None, children: List[ForwardRef('Node')], name: str | None)

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) → CommandNoncomputablesectionNode

name: str | None

class lean_dojo.data_extraction.ast.CommandOpaqueNode(lean_file: lean_dojo.data_extraction.lean.LeanFile, start: lean_dojo.data_extraction.lean.Pos | None, end: lean_dojo.data_extraction.lean.Pos | None, children: List[ForwardRef('Node')], name: str)

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) → CommandOpaqueNode

name: str

class lean_dojo.data_extraction.ast.CommandOpenNode(lean_file: lean_dojo.data_extraction.lean.LeanFile, start: lean_dojo.data_extraction.lean.Pos | None, end: lean_dojo.data_extraction.lean.Pos | None, children: List[ForwardRef('Node')])

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) → CommandOpenNode

class lean_dojo.data_extraction.ast.CommandOpenonlyNode(lean_file: lean_dojo.data_extraction.lean.LeanFile, start: lean_dojo.data_extraction.lean.Pos | None, end: lean_dojo.data_extraction.lean.Pos | None, children: List[ForwardRef('Node')])

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) → CommandOpenonlyNode

class lean_dojo.data_extraction.ast.CommandPrivateNode(lean_file: lean_dojo.data_extraction.lean.LeanFile, start: lean_dojo.data_extraction.lean.Pos | None, end: lean_dojo.data_extraction.lean.Pos | None, children: List[ForwardRef('Node')])

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) → CommandPrivateNode

class lean_dojo.data_extraction.ast.CommandSectionNode(lean_file: lean_dojo.data_extraction.lean.LeanFile, start: lean_dojo.data_extraction.lean.Pos | None, end: lean_dojo.data_extraction.lean.Pos | None, children: List[ForwardRef('Node')], name: str | None)

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) → CommandNamespaceNode

name: str | None

class lean_dojo.data_extraction.ast.CommandStructureNode(lean_file: lean_dojo.data_extraction.lean.LeanFile, start: lean_dojo.data_extraction.lean.Pos | None, end: lean_dojo.data_extraction.lean.Pos | None, children: List[ForwardRef('Node')], name: str)

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) → CommandStructureNode

name: str

class lean_dojo.data_extraction.ast.CommandStructuretkNode(lean_file: lean_dojo.data_extraction.lean.LeanFile, start: lean_dojo.data_extraction.lean.Pos | None, end: lean_dojo.data_extraction.lean.Pos | None, children: List[ForwardRef('Node')])

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) → CommandStructuretkNode

class lean_dojo.data_extraction.ast.CommandTheoremNode(lean_file: lean_dojo.data_extraction.lean.LeanFile, start: lean_dojo.data_extraction.lean.Pos | None, end: lean_dojo.data_extraction.lean.Pos | None, children: List[ForwardRef('Node')], name: str, full_name: str | None = None, _is_private_decl: bool | None = False)

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) → CommandTheoremNode

full_name: str | None = None

get_proof_node() → Node

has_tactic_proof() → bool

property is_mutual: bool

is_private() → bool

name: str

class lean_dojo.data_extraction.ast.CommandWherestructinstNode(lean_file: lean_dojo.data_extraction.lean.LeanFile, start: lean_dojo.data_extraction.lean.Pos | None, end: lean_dojo.data_extraction.lean.Pos | None, children: List[ForwardRef('Node')])

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) → CommandWherestructinstNode

class lean_dojo.data_extraction.ast.FileNode(lean_file: lean_dojo.data_extraction.lean.LeanFile, start: lean_dojo.data_extraction.lean.Pos | None, end: lean_dojo.data_extraction.lean.Pos | None, children: List[ForwardRef('Node')])

Bases: Node

classmethod from_data(data: Dict[str, Any], lean_file: LeanFile) → FileNode

class lean_dojo.data_extraction.ast.GroupNode(lean_file: lean_dojo.data_extraction.lean.LeanFile, start: lean_dojo.data_extraction.lean.Pos | None, end: lean_dojo.data_extraction.lean.Pos | None, children: List[ForwardRef('Node')])

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) → GroupNode

class lean_dojo.data_extraction.ast.IdentAntiquotNode(lean_file: lean_dojo.data_extraction.lean.LeanFile, start: lean_dojo.data_extraction.lean.Pos | None, end: lean_dojo.data_extraction.lean.Pos | None, children: List[ForwardRef('Node')])

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) → IdentAntiquotNode

get_ident() → str

class lean_dojo.data_extraction.ast.IdentNode(lean_file: lean_dojo.data_extraction.lean.LeanFile, start: lean_dojo.data_extraction.lean.Pos | None, end: lean_dojo.data_extraction.lean.Pos | None, children: List[ForwardRef('Node')], leading: str, trailing: str, raw_val: str, val: str, full_name: str | None = None, mod_name: str | None = None, def_path: str | None = None, def_start: lean_dojo.data_extraction.lean.Pos | None = None, def_end: lean_dojo.data_extraction.lean.Pos | None = None)

Bases: Node

def_end: Pos | None = None

def_path: str | None = None

def_start: Pos | None = None

classmethod from_data(ident_data: Dict[str, Any], lean_file: LeanFile) → IdentNode | None

full_name: str | None = None

property is_mutual: bool

leading: str

mod_name: str | None = None

raw_val: str

trailing: str

val: str

class lean_dojo.data_extraction.ast.LeanBinderidentAntiquotNode(lean_file: lean_dojo.data_extraction.lean.LeanFile, start: lean_dojo.data_extraction.lean.Pos | None, end: lean_dojo.data_extraction.lean.Pos | None, children: List[ForwardRef('Node')])

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) → LeanBinderidentAntiquotNode

get_ident() → str | None

class lean_dojo.data_extraction.ast.LeanBinderidentNode(lean_file: lean_dojo.data_extraction.lean.LeanFile, start: lean_dojo.data_extraction.lean.Pos | None, end: lean_dojo.data_extraction.lean.Pos | None, children: List[ForwardRef('Node')])

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) → LeanBinderidentNode

get_ident() → str | None

class lean_dojo.data_extraction.ast.LeanElabCommandCommandIrreducibleDefNode(lean_file: lean_dojo.data_extraction.lean.LeanFile, start: lean_dojo.data_extraction.lean.Pos | None, end: lean_dojo.data_extraction.lean.Pos | None, children: List[ForwardRef('Node')], name: str | None, full_name: str | None = None)

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) → LeanElabCommandCommandIrreducibleDefNode

full_name: str | None = None

name: str | None

class lean_dojo.data_extraction.ast.LemmaNode(lean_file: lean_dojo.data_extraction.lean.LeanFile, start: lean_dojo.data_extraction.lean.Pos | None, end: lean_dojo.data_extraction.lean.Pos | None, children: List[ForwardRef('Node')], name: str, full_name: str | None = None, _is_private_decl: bool | None = False)

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) → LemmaNode

full_name: str | None = None

get_proof_node() → Node

has_tactic_proof() → bool

property is_mutual: bool

is_private() → bool

name: str

class lean_dojo.data_extraction.ast.MathlibTacticLemmaNode(lean_file: lean_dojo.data_extraction.lean.LeanFile, start: lean_dojo.data_extraction.lean.Pos | None, end: lean_dojo.data_extraction.lean.Pos | None, children: List[ForwardRef('Node')], name: str, full_name: str | None = None, _is_private_decl: bool | None = False)

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) → MathlibTacticLemmaNode

full_name: str | None = None

get_proof_node() → Node

has_tactic_proof() → bool

property is_mutual: bool

is_private() → bool

name: str

class lean_dojo.data_extraction.ast.ModuleHeaderNode(lean_file: lean_dojo.data_extraction.lean.LeanFile, start: lean_dojo.data_extraction.lean.Pos | None, end: lean_dojo.data_extraction.lean.Pos | None, children: List[ForwardRef('Node')])

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) → ModuleHeaderNode

class lean_dojo.data_extraction.ast.ModuleImportNode(lean_file: lean_dojo.data_extraction.lean.LeanFile, start: lean_dojo.data_extraction.lean.Pos | None, end: lean_dojo.data_extraction.lean.Pos | None, children: List[ForwardRef('Node')], module: str | None, path: pathlib.Path | None = None)

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) → ModuleImportNode

module: str | None

path: Path | None = None

class lean_dojo.data_extraction.ast.ModulePreludeNode(lean_file: lean_dojo.data_extraction.lean.LeanFile, start: lean_dojo.data_extraction.lean.Pos | None, end: lean_dojo.data_extraction.lean.Pos | None, children: List[ForwardRef('Node')])

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) → ModulePreludeNode

class lean_dojo.data_extraction.ast.Node(lean_file: lean_dojo.data_extraction.lean.LeanFile, start: lean_dojo.data_extraction.lean.Pos | None, end: lean_dojo.data_extraction.lean.Pos | None, children: List[ForwardRef('Node')])

Bases: object

children: List[Node]

end: Pos | None

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) → Node

classmethod from_xml(tree: Element, lean_file: LeanFile) → Node

get_closure() → Tuple[Pos | None, Pos | None]

classmethod kind() → str

lean_file: LeanFile

start: Pos | None

to_xml(parent: Element) → None

traverse_postorder(callback: Callable[[Node, List[Any]], Any]) → Any

traverse_preorder(callback: Callable[[Node, List[Node]], Any], node_cls: type | None, parents: List[Node] = []) → None

class lean_dojo.data_extraction.ast.NullNode(lean_file: lean_dojo.data_extraction.lean.LeanFile, start: lean_dojo.data_extraction.lean.Pos | None, end: lean_dojo.data_extraction.lean.Pos | None, children: List[ForwardRef('Node')])

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) → NullNode

class lean_dojo.data_extraction.ast.OtherNode(lean_file: lean_dojo.data_extraction.lean.LeanFile, start: Optional[lean_dojo.data_extraction.lean.Pos], end: Optional[lean_dojo.data_extraction.lean.Pos], children: List[ForwardRef('Node')], kind: str = <bound method Node.kind of <class 'lean_dojo.data_extraction.ast.OtherNode'>>, state_before: Optional[str] = None, state_after: Optional[str] = None, tactic: Optional[str] = None)

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) → OtherNode

state_after: str | None = None

state_before: str | None = None

tactic: str | None = None

class lean_dojo.data_extraction.ast.StdTacticAliasAliasNode(lean_file: lean_dojo.data_extraction.lean.LeanFile, start: lean_dojo.data_extraction.lean.Pos | None, end: lean_dojo.data_extraction.lean.Pos | None, children: List[ForwardRef('Node')], name: str, full_name: str | None = None)

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) → StdTacticAliasAliasNode

full_name: str | None = None

name: str

class lean_dojo.data_extraction.ast.StdTacticAliasAliaslrNode(lean_file: lean_dojo.data_extraction.lean.LeanFile, start: lean_dojo.data_extraction.lean.Pos | None, end: lean_dojo.data_extraction.lean.Pos | None, children: List[ForwardRef('Node')], name: List[str], full_name: List[str] | None = None)

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) → StdTacticAliasAliaslrNode

full_name: List[str] | None = None

property is_mutual: bool

name: List[str]

class lean_dojo.data_extraction.ast.TacticTacticseq1IndentedAntiquotNode(lean_file: lean_dojo.data_extraction.lean.LeanFile, start: lean_dojo.data_extraction.lean.Pos | None, end: lean_dojo.data_extraction.lean.Pos | None, children: List[ForwardRef('Node')])

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) → TacticTacticseq1IndentedAntiquotNode

get_tactic_nodes(atomic_only: bool = False) → Generator[Node, None, None]

class lean_dojo.data_extraction.ast.TacticTacticseq1IndentedNode(lean_file: lean_dojo.data_extraction.lean.LeanFile, start: lean_dojo.data_extraction.lean.Pos | None, end: lean_dojo.data_extraction.lean.Pos | None, children: List[ForwardRef('Node')])

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) → TacticTacticseq1IndentedNode

get_tactic_nodes(atomic_only: bool = False) → Generator[Node, None, None]

class lean_dojo.data_extraction.ast.TacticTacticseqNode(lean_file: lean_dojo.data_extraction.lean.LeanFile, start: lean_dojo.data_extraction.lean.Pos | None, end: lean_dojo.data_extraction.lean.Pos | None, children: List[ForwardRef('Node')])

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) → TacticTacticseqNode

get_tactic_nodes(atomic_only: bool = False) → Generator[Node, None, None]

class lean_dojo.data_extraction.ast.TacticTacticseqbracketedNode(lean_file: lean_dojo.data_extraction.lean.LeanFile, start: lean_dojo.data_extraction.lean.Pos | None, end: lean_dojo.data_extraction.lean.Pos | None, children: List[ForwardRef('Node')], state_before: str | None = None, state_after: str | None = None, tactic: str | None = None)

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) → TacticTacticseqbracketedNode

get_tactic_nodes(atomic_only: bool = False) → Generator[Node, None, None]

state_after: str | None = None

state_before: str | None = None

tactic: str | None = None

property tactic_nodes: List[Node]

class lean_dojo.data_extraction.ast.TermAttrkindAntiquotNode(lean_file: lean_dojo.data_extraction.lean.LeanFile, start: lean_dojo.data_extraction.lean.Pos | None, end: lean_dojo.data_extraction.lean.Pos | None, children: List[ForwardRef('Node')])

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) → TermAttrkindAntiquotNode

class lean_dojo.data_extraction.ast.TermAttrkindNode(lean_file: lean_dojo.data_extraction.lean.LeanFile, start: lean_dojo.data_extraction.lean.Pos | None, end: lean_dojo.data_extraction.lean.Pos | None, children: List[ForwardRef('Node')])

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) → TermAttrkindNode

class lean_dojo.data_extraction.ast.TermBytacticNode(lean_file: lean_dojo.data_extraction.lean.LeanFile, start: lean_dojo.data_extraction.lean.Pos | None, end: lean_dojo.data_extraction.lean.Pos | None, children: List[ForwardRef('Node')])

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) → TermBytacticNode

class lean_dojo.data_extraction.ast.TermExplicitbinderNode(lean_file: lean_dojo.data_extraction.lean.LeanFile, start: lean_dojo.data_extraction.lean.Pos | None, end: lean_dojo.data_extraction.lean.Pos | None, children: List[ForwardRef('Node')])

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) → TermExplicitbinderNode

class lean_dojo.data_extraction.ast.TermHoleNode(lean_file: lean_dojo.data_extraction.lean.LeanFile, start: lean_dojo.data_extraction.lean.Pos | None, end: lean_dojo.data_extraction.lean.Pos | None, children: List[ForwardRef('Node')])

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) → TermHoleNode

class lean_dojo.data_extraction.ast.TermTypespecNode(lean_file: lean_dojo.data_extraction.lean.LeanFile, start: lean_dojo.data_extraction.lean.Pos | None, end: lean_dojo.data_extraction.lean.Pos | None, children: List[ForwardRef('Node')])

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) → TermTypespecNode

class lean_dojo.data_extraction.ast.TokenAntiquotNode(lean_file: lean_dojo.data_extraction.lean.LeanFile, start: lean_dojo.data_extraction.lean.Pos | None, end: lean_dojo.data_extraction.lean.Pos | None, children: List[ForwardRef('Node')])

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) → TokenAntiquotNode

lean_dojo.data_extraction.ast.contains_tactic(node: Node) → bool

lean_dojo.data_extraction.ast.is_leaf(node: Node) → bool

lean_dojo.data_extraction.ast.is_mutual_lean4(node: Node) → bool

lean_dojo.data_extraction.ast.is_potential_premise_lean4(node: Node) → bool

Check if node is a theorem/definition that can be used as a premise.