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)[source]

Bases: Node

classmethod from_data(atom_data: Dict[str, Any], lean_file: LeanFile) AtomNode | None[source]
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)[source]

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) CommandAbbrevNode[source]
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)[source]

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) CommandAxiomNode[source]
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)[source]

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) CommandClassinductiveNode[source]
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')])[source]

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) CommandClasstkNode[source]
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)[source]

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) CommandDeclarationNode[source]
full_name: str | None = None
get_theorem_node() CommandTheoremNode[source]
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')])[source]

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) CommandDeclidAntiquotNode[source]
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')])[source]

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) CommandDeclidNode[source]
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')])[source]

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) CommandDeclmodifiersAntiquotNode[source]
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')])[source]

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) CommandDeclmodifiersNode[source]
is_private() bool[source]
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')])[source]

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) CommandDeclsigNode[source]
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')])[source]

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) CommandDeclvaleqnsNode[source]
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')])[source]

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) CommandDeclvalsimpleNode[source]
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)[source]

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) CommandDefNode[source]
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)[source]

Bases: Node

comment: str
classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) CommandDoccommentNode[source]
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)[source]

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) CommandEndNode[source]
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)[source]

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) CommandExampleNode[source]
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)[source]

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) CommandInductiveNode[source]
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)[source]

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) CommandInstanceNode[source]
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)[source]

Bases: Node

comment: str
classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) CommandModuledocNode[source]
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)[source]

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) CommandNamespaceNode[source]
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)[source]

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) CommandNoncomputablesectionNode[source]
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)[source]

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) CommandOpaqueNode[source]
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')])[source]

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) CommandOpenNode[source]
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')])[source]

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) CommandOpenonlyNode[source]
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')])[source]

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) CommandPrivateNode[source]
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)[source]

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) CommandNamespaceNode[source]
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)[source]

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) CommandStructureNode[source]
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')])[source]

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) CommandStructuretkNode[source]
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)[source]

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) CommandTheoremNode[source]
full_name: str | None = None
get_proof_node() Node[source]
has_tactic_proof() bool[source]
property is_mutual: bool
is_private() bool[source]
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')])[source]

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) CommandWherestructinstNode[source]
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')])[source]

Bases: Node

classmethod from_data(data: Dict[str, Any], lean_file: LeanFile) FileNode[source]
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')])[source]

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) GroupNode[source]
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')])[source]

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) IdentAntiquotNode[source]
get_ident() str[source]
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)[source]

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[source]
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')])[source]

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) LeanBinderidentAntiquotNode[source]
get_ident() str | None[source]
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')])[source]

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) LeanBinderidentNode[source]
get_ident() str | None[source]
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)[source]

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) LeanElabCommandCommandIrreducibleDefNode[source]
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)[source]

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) LemmaNode[source]
full_name: str | None = None
get_proof_node() Node[source]
has_tactic_proof() bool[source]
property is_mutual: bool
is_private() bool[source]
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)[source]

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) MathlibTacticLemmaNode[source]
full_name: str | None = None
get_proof_node() Node[source]
has_tactic_proof() bool[source]
property is_mutual: bool
is_private() bool[source]
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')])[source]

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) ModuleHeaderNode[source]
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)[source]

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) ModuleImportNode[source]
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')])[source]

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) ModulePreludeNode[source]
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')])[source]

Bases: object

children: List[Node]
end: Pos | None
classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) Node[source]
classmethod from_xml(tree: Element, lean_file: LeanFile) Node[source]
get_closure() Tuple[Pos, Pos][source]
classmethod kind() str[source]
lean_file: LeanFile
start: Pos | None
to_xml(parent: Element) None[source]
traverse_postorder(callback: Callable[[Node, List[Any]], Any]) Any[source]
traverse_preorder(callback: Callable[[Node, List[Node]], Any], node_cls: type | None, parents: List[Node] = []) None[source]
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')])[source]

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) NullNode[source]
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)[source]

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) OtherNode[source]
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)[source]

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) StdTacticAliasAliasNode[source]
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)[source]

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) StdTacticAliasAliaslrNode[source]
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')])[source]

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) TacticTacticseq1IndentedAntiquotNode[source]
get_tactic_nodes(atomic_only: bool = False) Generator[Node, None, None][source]
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')])[source]

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) TacticTacticseq1IndentedNode[source]
get_tactic_nodes(atomic_only: bool = False) Generator[Node, None, None][source]
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')])[source]

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) TacticTacticseqNode[source]
get_tactic_nodes(atomic_only: bool = False) Generator[Node, None, None][source]
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)[source]

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) TacticTacticseqbracketedNode[source]
get_tactic_nodes(atomic_only: bool = False) Generator[Node, None, None][source]
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')])[source]

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) TermAttrkindAntiquotNode[source]
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')])[source]

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) TermAttrkindNode[source]
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')])[source]

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) TermBytacticNode[source]
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')])[source]

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) TermExplicitbinderNode[source]
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')])[source]

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) TermHoleNode[source]
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')])[source]

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) TermTypespecNode[source]
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')])[source]

Bases: Node

classmethod from_data(node_data: Dict[str, Any], lean_file: LeanFile) TokenAntiquotNode[source]
lean_dojo.data_extraction.ast.contains_tactic(node: Node) bool[source]
lean_dojo.data_extraction.ast.is_leaf(node: Node) bool[source]
lean_dojo.data_extraction.ast.is_mutual_lean4(node: Node) bool[source]
lean_dojo.data_extraction.ast.is_potential_premise_lean4(node: Node) bool[source]

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