LeanDojo
latest
Getting Started
User Guide
Troubleshooting
Developer Guide
Limitations and Caveats
Credits and Acknowledgements
API Reference
LeanDojo
Index
Edit on GitHub
Index
_
|
A
|
C
|
D
|
E
|
F
|
G
|
H
|
I
|
K
|
L
|
M
|
N
|
O
|
P
|
R
|
S
|
T
|
U
|
V
_
__getitem__() (lean_dojo.data_extraction.lean.LeanFile method)
A
abs_path (lean_dojo.data_extraction.lean.LeanFile property)
(lean_dojo.data_extraction.traced_data.TracedFile property)
additional_imports (lean_dojo.interaction.dojo.Dojo attribute)
assumptions (lean_dojo.interaction.parse_goals.Goal attribute)
ast (lean_dojo.data_extraction.traced_data.TracedFile attribute)
(lean_dojo.data_extraction.traced_data.TracedTactic attribute)
(lean_dojo.data_extraction.traced_data.TracedTheorem attribute)
AtomNode (class in lean_dojo.data_extraction.ast)
C
CACHE_DIR (in module lean_dojo.constants)
check_git_version() (in module lean_dojo.constants)
check_sanity() (lean_dojo.data_extraction.traced_data.TracedFile method)
(lean_dojo.data_extraction.traced_data.TracedRepo method)
children (lean_dojo.data_extraction.ast.Node attribute)
cleanse_string() (in module lean_dojo.data_extraction.lean)
clone_and_checkout() (lean_dojo.data_extraction.lean.LeanGitRepo method)
code (lean_dojo.data_extraction.lean.LeanFile attribute)
column_nb (lean_dojo.data_extraction.lean.Pos attribute)
CommandAbbrevNode (class in lean_dojo.data_extraction.ast)
CommandAxiomNode (class in lean_dojo.data_extraction.ast)
CommandClassinductiveNode (class in lean_dojo.data_extraction.ast)
CommandClasstkNode (class in lean_dojo.data_extraction.ast)
CommandDeclarationNode (class in lean_dojo.data_extraction.ast)
CommandDeclidAntiquotNode (class in lean_dojo.data_extraction.ast)
CommandDeclidNode (class in lean_dojo.data_extraction.ast)
CommandDeclmodifiersAntiquotNode (class in lean_dojo.data_extraction.ast)
CommandDeclmodifiersNode (class in lean_dojo.data_extraction.ast)
CommandDeclsigNode (class in lean_dojo.data_extraction.ast)
CommandDeclvaleqnsNode (class in lean_dojo.data_extraction.ast)
CommandDeclvalsimpleNode (class in lean_dojo.data_extraction.ast)
CommandDefNode (class in lean_dojo.data_extraction.ast)
CommandDoccommentNode (class in lean_dojo.data_extraction.ast)
CommandEndNode (class in lean_dojo.data_extraction.ast)
CommandExampleNode (class in lean_dojo.data_extraction.ast)
CommandInductiveNode (class in lean_dojo.data_extraction.ast)
CommandInstanceNode (class in lean_dojo.data_extraction.ast)
CommandModuledocNode (class in lean_dojo.data_extraction.ast)
CommandNamespaceNode (class in lean_dojo.data_extraction.ast)
CommandNoncomputablesectionNode (class in lean_dojo.data_extraction.ast)
CommandOpaqueNode (class in lean_dojo.data_extraction.ast)
CommandOpenNode (class in lean_dojo.data_extraction.ast)
CommandOpenonlyNode (class in lean_dojo.data_extraction.ast)
CommandPrivateNode (class in lean_dojo.data_extraction.ast)
CommandSectionNode (class in lean_dojo.data_extraction.ast)
CommandState (class in lean_dojo.interaction.dojo)
CommandStructureNode (class in lean_dojo.data_extraction.ast)
CommandStructuretkNode (class in lean_dojo.data_extraction.ast)
CommandTheoremNode (class in lean_dojo.data_extraction.ast)
CommandWherestructinstNode (class in lean_dojo.data_extraction.ast)
Comment (class in lean_dojo.data_extraction.traced_data)
comment (lean_dojo.data_extraction.ast.CommandDoccommentNode attribute)
(lean_dojo.data_extraction.ast.CommandModuledocNode attribute)
comments (lean_dojo.data_extraction.traced_data.TracedFile attribute)
(lean_dojo.data_extraction.traced_data.TracedTheorem attribute)
commit (lean_dojo.data_extraction.lean.LeanGitRepo attribute)
commit_url (lean_dojo.data_extraction.lean.LeanGitRepo property)
conclusion (lean_dojo.interaction.parse_goals.Goal attribute)
CONTAINER (in module lean_dojo.constants)
contains_tactic() (in module lean_dojo.data_extraction.ast)
convert_pos() (lean_dojo.data_extraction.lean.LeanFile method)
D
Declaration (class in lean_dojo.interaction.parse_goals)
def_end (lean_dojo.data_extraction.ast.IdentNode attribute)
def_path (lean_dojo.data_extraction.ast.IdentNode attribute)
def_start (lean_dojo.data_extraction.ast.IdentNode attribute)
dependencies (lean_dojo.data_extraction.traced_data.TracedRepo attribute)
DISABLE_REMOTE_CACHE (in module lean_dojo.constants)
Dojo (class in lean_dojo.interaction.dojo)
DojoCrashError
DojoHardTimeoutError
DojoInitError
E
end (lean_dojo.data_extraction.ast.Node attribute)
(lean_dojo.data_extraction.traced_data.Comment attribute)
(lean_dojo.data_extraction.traced_data.TracedTactic property)
(lean_dojo.data_extraction.traced_data.TracedTheorem property)
end_pos (lean_dojo.data_extraction.lean.LeanFile property)
endwith_newline (lean_dojo.data_extraction.lean.LeanFile attribute)
entry (lean_dojo.interaction.dojo.Dojo attribute)
error (lean_dojo.interaction.dojo.LeanError attribute)
(lean_dojo.interaction.dojo.TimeoutError attribute)
exists() (lean_dojo.data_extraction.lean.LeanGitRepo method)
F
file_path (lean_dojo.data_extraction.lean.Theorem attribute)
(lean_dojo.data_extraction.traced_data.TracedTheorem property)
(lean_dojo.interaction.dojo.Dojo attribute)
FileNode (class in lean_dojo.data_extraction.ast)
from_data() (lean_dojo.data_extraction.ast.AtomNode class method)
(lean_dojo.data_extraction.ast.CommandAbbrevNode class method)
(lean_dojo.data_extraction.ast.CommandAxiomNode class method)
(lean_dojo.data_extraction.ast.CommandClassinductiveNode class method)
(lean_dojo.data_extraction.ast.CommandClasstkNode class method)
(lean_dojo.data_extraction.ast.CommandDeclarationNode class method)
(lean_dojo.data_extraction.ast.CommandDeclidAntiquotNode class method)
(lean_dojo.data_extraction.ast.CommandDeclidNode class method)
(lean_dojo.data_extraction.ast.CommandDeclmodifiersAntiquotNode class method)
(lean_dojo.data_extraction.ast.CommandDeclmodifiersNode class method)
(lean_dojo.data_extraction.ast.CommandDeclsigNode class method)
(lean_dojo.data_extraction.ast.CommandDeclvaleqnsNode class method)
(lean_dojo.data_extraction.ast.CommandDeclvalsimpleNode class method)
(lean_dojo.data_extraction.ast.CommandDefNode class method)
(lean_dojo.data_extraction.ast.CommandDoccommentNode class method)
(lean_dojo.data_extraction.ast.CommandEndNode class method)
(lean_dojo.data_extraction.ast.CommandExampleNode class method)
(lean_dojo.data_extraction.ast.CommandInductiveNode class method)
(lean_dojo.data_extraction.ast.CommandInstanceNode class method)
(lean_dojo.data_extraction.ast.CommandModuledocNode class method)
(lean_dojo.data_extraction.ast.CommandNamespaceNode class method)
(lean_dojo.data_extraction.ast.CommandNoncomputablesectionNode class method)
(lean_dojo.data_extraction.ast.CommandOpaqueNode class method)
(lean_dojo.data_extraction.ast.CommandOpenNode class method)
(lean_dojo.data_extraction.ast.CommandOpenonlyNode class method)
(lean_dojo.data_extraction.ast.CommandPrivateNode class method)
(lean_dojo.data_extraction.ast.CommandSectionNode class method)
(lean_dojo.data_extraction.ast.CommandStructureNode class method)
(lean_dojo.data_extraction.ast.CommandStructuretkNode class method)
(lean_dojo.data_extraction.ast.CommandTheoremNode class method)
(lean_dojo.data_extraction.ast.CommandWherestructinstNode class method)
(lean_dojo.data_extraction.ast.FileNode class method)
(lean_dojo.data_extraction.ast.GroupNode class method)
(lean_dojo.data_extraction.ast.IdentAntiquotNode class method)
(lean_dojo.data_extraction.ast.IdentNode class method)
(lean_dojo.data_extraction.ast.LeanBinderidentAntiquotNode class method)
(lean_dojo.data_extraction.ast.LeanBinderidentNode class method)
(lean_dojo.data_extraction.ast.LeanElabCommandCommandIrreducibleDefNode class method)
(lean_dojo.data_extraction.ast.LemmaNode class method)
(lean_dojo.data_extraction.ast.MathlibTacticLemmaNode class method)
(lean_dojo.data_extraction.ast.ModuleHeaderNode class method)
(lean_dojo.data_extraction.ast.ModuleImportNode class method)
(lean_dojo.data_extraction.ast.ModulePreludeNode class method)
(lean_dojo.data_extraction.ast.Node class method)
(lean_dojo.data_extraction.ast.NullNode class method)
(lean_dojo.data_extraction.ast.OtherNode class method)
(lean_dojo.data_extraction.ast.StdTacticAliasAliaslrNode class method)
(lean_dojo.data_extraction.ast.StdTacticAliasAliasNode class method)
(lean_dojo.data_extraction.ast.TacticTacticseq1IndentedAntiquotNode class method)
(lean_dojo.data_extraction.ast.TacticTacticseq1IndentedNode class method)
(lean_dojo.data_extraction.ast.TacticTacticseqbracketedNode class method)
(lean_dojo.data_extraction.ast.TacticTacticseqNode class method)
(lean_dojo.data_extraction.ast.TermAttrkindAntiquotNode class method)
(lean_dojo.data_extraction.ast.TermAttrkindNode class method)
(lean_dojo.data_extraction.ast.TermBytacticNode class method)
(lean_dojo.data_extraction.ast.TermExplicitbinderNode class method)
(lean_dojo.data_extraction.ast.TermHoleNode class method)
(lean_dojo.data_extraction.ast.TermTypespecNode class method)
(lean_dojo.data_extraction.ast.TokenAntiquotNode class method)
from_path() (lean_dojo.data_extraction.lean.LeanGitRepo class method)
from_pp() (lean_dojo.interaction.parse_goals.Goal class method)
from_str() (lean_dojo.data_extraction.lean.Pos class method)
from_traced_file() (lean_dojo.data_extraction.traced_data.TracedFile class method)
from_traced_files() (lean_dojo.data_extraction.traced_data.TracedRepo class method)
from_xml() (lean_dojo.data_extraction.ast.Node class method)
(lean_dojo.data_extraction.traced_data.Comment class method)
(lean_dojo.data_extraction.traced_data.TracedFile class method)
full_name (lean_dojo.data_extraction.ast.CommandDeclarationNode attribute)
(lean_dojo.data_extraction.ast.CommandTheoremNode attribute)
(lean_dojo.data_extraction.ast.IdentNode attribute)
(lean_dojo.data_extraction.ast.LeanElabCommandCommandIrreducibleDefNode attribute)
(lean_dojo.data_extraction.ast.LemmaNode attribute)
(lean_dojo.data_extraction.ast.MathlibTacticLemmaNode attribute)
(lean_dojo.data_extraction.ast.StdTacticAliasAliaslrNode attribute)
(lean_dojo.data_extraction.ast.StdTacticAliasAliasNode attribute)
(lean_dojo.data_extraction.lean.Theorem attribute)
G
get_annotated_tactic() (lean_dojo.data_extraction.traced_data.TracedTactic method)
get_closure() (lean_dojo.data_extraction.ast.Node method)
get_code_without_comments() (in module lean_dojo.data_extraction.traced_data)
get_config() (lean_dojo.data_extraction.lean.LeanGitRepo method)
get_dependencies() (lean_dojo.data_extraction.lean.LeanGitRepo method)
get_direct_dependencies() (lean_dojo.data_extraction.traced_data.TracedFile method)
get_ident() (lean_dojo.data_extraction.ast.IdentAntiquotNode method)
(lean_dojo.data_extraction.ast.LeanBinderidentAntiquotNode method)
(lean_dojo.data_extraction.ast.LeanBinderidentNode method)
get_latest_commit() (in module lean_dojo.data_extraction.lean)
get_lean4_commit_from_config() (in module lean_dojo.data_extraction.lean)
get_lean4_version_from_config() (in module lean_dojo.data_extraction.lean)
get_license() (lean_dojo.data_extraction.lean.LeanGitRepo method)
get_line() (lean_dojo.data_extraction.lean.LeanFile method)
get_namespaces() (lean_dojo.data_extraction.traced_data.TracedTheorem method)
get_num_tactics() (lean_dojo.data_extraction.traced_data.TracedTheorem method)
get_premise_definitions() (lean_dojo.data_extraction.traced_data.TracedFile method)
get_premise_full_names() (lean_dojo.data_extraction.traced_data.TracedTheorem method)
get_proof_node() (lean_dojo.data_extraction.ast.CommandTheoremNode method)
(lean_dojo.data_extraction.ast.LemmaNode method)
(lean_dojo.data_extraction.ast.MathlibTacticLemmaNode method)
(lean_dojo.data_extraction.traced_data.TracedTheorem method)
get_single_tactic_proof() (lean_dojo.data_extraction.traced_data.TracedTheorem method)
get_tactic_nodes() (lean_dojo.data_extraction.ast.TacticTacticseq1IndentedAntiquotNode method)
(lean_dojo.data_extraction.ast.TacticTacticseq1IndentedNode method)
(lean_dojo.data_extraction.ast.TacticTacticseqbracketedNode method)
(lean_dojo.data_extraction.ast.TacticTacticseqNode method)
get_tactic_proof() (lean_dojo.data_extraction.traced_data.TracedTheorem method)
get_theorem_node() (lean_dojo.data_extraction.ast.CommandDeclarationNode method)
get_theorem_statement() (lean_dojo.data_extraction.traced_data.TracedTheorem method)
get_traced_file() (lean_dojo.data_extraction.traced_data.TracedRepo method)
get_traced_repo_path() (in module lean_dojo.data_extraction.trace)
get_traced_tactics() (lean_dojo.data_extraction.traced_data.TracedTheorem method)
get_traced_theorem() (lean_dojo.data_extraction.traced_data.TracedFile method)
(lean_dojo.data_extraction.traced_data.TracedRepo method)
get_traced_theorems() (lean_dojo.data_extraction.traced_data.TracedFile method)
(lean_dojo.data_extraction.traced_data.TracedRepo method)
GITHUB_ACCESS_TOKEN (in module lean_dojo.data_extraction.lean)
Goal (class in lean_dojo.interaction.parse_goals)
goals (lean_dojo.interaction.dojo.TacticState attribute)
GroupNode (class in lean_dojo.data_extraction.ast)
H
hard_timeout (lean_dojo.interaction.dojo.Dojo attribute)
has_prelude (lean_dojo.data_extraction.traced_data.TracedFile property)
has_tactic_proof() (lean_dojo.data_extraction.ast.CommandTheoremNode method)
(lean_dojo.data_extraction.ast.LemmaNode method)
(lean_dojo.data_extraction.ast.MathlibTacticLemmaNode method)
(lean_dojo.data_extraction.traced_data.TracedTheorem method)
has_timedout (lean_dojo.interaction.dojo.Dojo attribute)
I
id (lean_dojo.interaction.dojo.CommandState attribute)
(lean_dojo.interaction.dojo.TacticState attribute)
ident (lean_dojo.interaction.parse_goals.Declaration attribute)
IdentAntiquotNode (class in lean_dojo.data_extraction.ast)
IdentNode (class in lean_dojo.data_extraction.ast)
is_available_in_cache() (in module lean_dojo.data_extraction.trace)
is_crashed (lean_dojo.interaction.dojo.Dojo attribute)
is_example (lean_dojo.data_extraction.ast.CommandDeclarationNode property)
is_leaf() (in module lean_dojo.data_extraction.ast)
is_lean4 (lean_dojo.data_extraction.lean.LeanGitRepo property)
is_mutual (lean_dojo.data_extraction.ast.CommandTheoremNode property)
(lean_dojo.data_extraction.ast.IdentNode property)
(lean_dojo.data_extraction.ast.LemmaNode property)
(lean_dojo.data_extraction.ast.MathlibTacticLemmaNode property)
(lean_dojo.data_extraction.ast.StdTacticAliasAliaslrNode property)
is_mutual_lean4() (in module lean_dojo.data_extraction.ast)
is_out_of_memory (lean_dojo.interaction.dojo.DojoCrashError property)
is_potential_premise_lean4() (in module lean_dojo.data_extraction.ast)
is_private (lean_dojo.data_extraction.traced_data.TracedTheorem property)
is_private() (lean_dojo.data_extraction.ast.CommandDeclmodifiersNode method)
(lean_dojo.data_extraction.ast.CommandTheoremNode method)
(lean_dojo.data_extraction.ast.LemmaNode method)
(lean_dojo.data_extraction.ast.MathlibTacticLemmaNode method)
is_successful (lean_dojo.interaction.dojo.Dojo attribute)
is_supported_version() (in module lean_dojo.data_extraction.lean)
is_theorem (lean_dojo.data_extraction.ast.CommandDeclarationNode property)
K
kind() (lean_dojo.data_extraction.ast.Node class method)
L
leading (lean_dojo.data_extraction.ast.AtomNode attribute)
(lean_dojo.data_extraction.ast.IdentNode attribute)
LEAN4_NIGHTLY_REPO (in module lean_dojo.data_extraction.lean)
LEAN4_PACKAGES_DIR (in module lean_dojo.constants)
LEAN4_REPO (in module lean_dojo.data_extraction.lean)
LEAN4_URL (in module lean_dojo.constants)
lean_dojo.constants
module
lean_dojo.data_extraction.ast
module
lean_dojo.data_extraction.lean
module
lean_dojo.data_extraction.trace
module
lean_dojo.data_extraction.traced_data
module
lean_dojo.interaction.dojo
module
lean_dojo.interaction.parse_goals
module
lean_file (lean_dojo.data_extraction.ast.Node attribute)
(lean_dojo.data_extraction.traced_data.TracedFile attribute)
lean_type (lean_dojo.interaction.parse_goals.Declaration attribute)
lean_version (lean_dojo.data_extraction.lean.LeanGitRepo attribute)
(lean_dojo.data_extraction.lean.RepoInfoCache attribute)
LeanBinderidentAntiquotNode (class in lean_dojo.data_extraction.ast)
LeanBinderidentNode (class in lean_dojo.data_extraction.ast)
LeanElabCommandCommandIrreducibleDefNode (class in lean_dojo.data_extraction.ast)
LeanError (class in lean_dojo.interaction.dojo)
LeanFile (class in lean_dojo.data_extraction.lean)
LeanGitRepo (class in lean_dojo.data_extraction.lean)
LemmaNode (class in lean_dojo.data_extraction.ast)
line_nb (lean_dojo.data_extraction.lean.Pos attribute)
load_from_disk() (lean_dojo.data_extraction.traced_data.TracedRepo class method)
LOAD_USED_PACKAGES_ONLY (in module lean_dojo.constants)
locate_proof() (lean_dojo.data_extraction.traced_data.TracedTheorem method)
M
MathlibTacticLemmaNode (class in lean_dojo.data_extraction.ast)
message (lean_dojo.interaction.dojo.CommandState attribute)
(lean_dojo.interaction.dojo.ProofFinished attribute)
(lean_dojo.interaction.dojo.TacticState attribute)
mod_name (lean_dojo.data_extraction.ast.IdentNode attribute)
module
lean_dojo.constants
lean_dojo.data_extraction.ast
lean_dojo.data_extraction.lean
lean_dojo.data_extraction.trace
lean_dojo.data_extraction.traced_data
lean_dojo.interaction.dojo
lean_dojo.interaction.parse_goals
module (lean_dojo.data_extraction.ast.ModuleImportNode attribute)
ModuleHeaderNode (class in lean_dojo.data_extraction.ast)
ModuleImportNode (class in lean_dojo.data_extraction.ast)
ModulePreludeNode (class in lean_dojo.data_extraction.ast)
N
name (lean_dojo.data_extraction.ast.CommandAbbrevNode attribute)
(lean_dojo.data_extraction.ast.CommandAxiomNode attribute)
(lean_dojo.data_extraction.ast.CommandClassinductiveNode attribute)
(lean_dojo.data_extraction.ast.CommandDeclarationNode attribute)
(lean_dojo.data_extraction.ast.CommandDefNode attribute)
(lean_dojo.data_extraction.ast.CommandEndNode attribute)
(lean_dojo.data_extraction.ast.CommandExampleNode attribute)
(lean_dojo.data_extraction.ast.CommandInductiveNode attribute)
(lean_dojo.data_extraction.ast.CommandInstanceNode attribute)
(lean_dojo.data_extraction.ast.CommandNamespaceNode attribute)
(lean_dojo.data_extraction.ast.CommandNoncomputablesectionNode attribute)
(lean_dojo.data_extraction.ast.CommandOpaqueNode attribute)
(lean_dojo.data_extraction.ast.CommandSectionNode attribute)
(lean_dojo.data_extraction.ast.CommandStructureNode attribute)
(lean_dojo.data_extraction.ast.CommandTheoremNode attribute)
(lean_dojo.data_extraction.ast.LeanElabCommandCommandIrreducibleDefNode attribute)
(lean_dojo.data_extraction.ast.LemmaNode attribute)
(lean_dojo.data_extraction.ast.MathlibTacticLemmaNode attribute)
(lean_dojo.data_extraction.ast.StdTacticAliasAliaslrNode attribute)
(lean_dojo.data_extraction.ast.StdTacticAliasAliasNode attribute)
(lean_dojo.data_extraction.lean.LeanGitRepo property)
(lean_dojo.data_extraction.traced_data.TracedRepo property)
Node (class in lean_dojo.data_extraction.ast)
normalize_url() (in module lean_dojo.data_extraction.lean)
NullNode (class in lean_dojo.data_extraction.ast)
num_bytes (lean_dojo.data_extraction.lean.LeanFile attribute)
num_columns() (lean_dojo.data_extraction.lean.LeanFile method)
num_goals (lean_dojo.interaction.dojo.TacticState property)
num_lines (lean_dojo.data_extraction.lean.LeanFile property)
NUM_PROCS (in module lean_dojo.constants)
O
offset() (lean_dojo.data_extraction.lean.LeanFile method)
OtherNode (class in lean_dojo.data_extraction.ast)
P
parse_goals() (in module lean_dojo.interaction.parse_goals)
path (lean_dojo.data_extraction.ast.ModuleImportNode attribute)
(lean_dojo.data_extraction.lean.LeanFile attribute)
(lean_dojo.data_extraction.traced_data.TracedFile property)
Pos (class in lean_dojo.data_extraction.lean)
pp (lean_dojo.interaction.dojo.TacticState attribute)
ProofFinished (class in lean_dojo.interaction.dojo)
ProofGivenUp (class in lean_dojo.interaction.dojo)
R
raw_val (lean_dojo.data_extraction.ast.IdentNode attribute)
REMOTE_CACHE_URL (in module lean_dojo.constants)
repo (lean_dojo.data_extraction.lean.LeanGitRepo attribute)
(lean_dojo.data_extraction.lean.Theorem attribute)
(lean_dojo.data_extraction.traced_data.TracedFile attribute)
(lean_dojo.data_extraction.traced_data.TracedRepo attribute)
(lean_dojo.data_extraction.traced_data.TracedTheorem property)
(lean_dojo.interaction.dojo.Dojo attribute)
RepoInfoCache (class in lean_dojo.data_extraction.lean)
root_dir (lean_dojo.data_extraction.lean.LeanFile attribute)
(lean_dojo.data_extraction.traced_data.TracedFile attribute)
(lean_dojo.data_extraction.traced_data.TracedRepo attribute)
(lean_dojo.data_extraction.traced_data.TracedTheorem attribute)
run_cmd() (lean_dojo.interaction.dojo.Dojo method)
run_tac() (lean_dojo.interaction.dojo.Dojo method)
S
save_to_disk() (lean_dojo.data_extraction.traced_data.TracedRepo method)
show() (lean_dojo.data_extraction.lean.LeanGitRepo method)
(lean_dojo.data_extraction.traced_data.TracedRepo method)
(lean_dojo.data_extraction.traced_data.TracedTheorem method)
start (lean_dojo.data_extraction.ast.Node attribute)
(lean_dojo.data_extraction.traced_data.Comment attribute)
(lean_dojo.data_extraction.traced_data.TracedTactic property)
(lean_dojo.data_extraction.traced_data.TracedTheorem property)
start_pos (lean_dojo.data_extraction.lean.LeanFile property)
state_after (lean_dojo.data_extraction.ast.OtherNode attribute)
(lean_dojo.data_extraction.ast.TacticTacticseqbracketedNode attribute)
(lean_dojo.data_extraction.traced_data.TracedTactic property)
state_before (lean_dojo.data_extraction.ast.OtherNode attribute)
(lean_dojo.data_extraction.ast.TacticTacticseqbracketedNode attribute)
(lean_dojo.data_extraction.traced_data.TracedTactic property)
StdTacticAliasAliaslrNode (class in lean_dojo.data_extraction.ast)
StdTacticAliasAliasNode (class in lean_dojo.data_extraction.ast)
T
tactic (lean_dojo.data_extraction.ast.OtherNode attribute)
(lean_dojo.data_extraction.ast.TacticTacticseqbracketedNode attribute)
(lean_dojo.data_extraction.traced_data.TracedTactic property)
TACTIC_CPU_LIMIT (in module lean_dojo.constants)
TACTIC_MEMORY_LIMIT (in module lean_dojo.constants)
tactic_nodes (lean_dojo.data_extraction.ast.TacticTacticseqbracketedNode property)
tactic_state_id (lean_dojo.interaction.dojo.ProofFinished attribute)
TacticState (class in lean_dojo.interaction.dojo)
TacticTacticseq1IndentedAntiquotNode (class in lean_dojo.data_extraction.ast)
TacticTacticseq1IndentedNode (class in lean_dojo.data_extraction.ast)
TacticTacticseqbracketedNode (class in lean_dojo.data_extraction.ast)
TacticTacticseqNode (class in lean_dojo.data_extraction.ast)
tag2commit (lean_dojo.data_extraction.lean.RepoInfoCache attribute)
TermAttrkindAntiquotNode (class in lean_dojo.data_extraction.ast)
TermAttrkindNode (class in lean_dojo.data_extraction.ast)
TermBytacticNode (class in lean_dojo.data_extraction.ast)
TermExplicitbinderNode (class in lean_dojo.data_extraction.ast)
TermHoleNode (class in lean_dojo.data_extraction.ast)
TermTypespecNode (class in lean_dojo.data_extraction.ast)
text (lean_dojo.data_extraction.traced_data.Comment attribute)
Theorem (class in lean_dojo.data_extraction.lean)
theorem (lean_dojo.data_extraction.traced_data.TracedTheorem attribute)
TimeoutError (class in lean_dojo.interaction.dojo)
TMP_DIR (in module lean_dojo.constants)
to_string() (lean_dojo.data_extraction.traced_data.TracedTactic method)
to_xml() (lean_dojo.data_extraction.ast.Node method)
(lean_dojo.data_extraction.traced_data.Comment method)
(lean_dojo.data_extraction.traced_data.TracedFile method)
TokenAntiquotNode (class in lean_dojo.data_extraction.ast)
trace() (in module lean_dojo.data_extraction.trace)
traced_file (lean_dojo.data_extraction.traced_data.TracedTheorem attribute)
traced_files (lean_dojo.data_extraction.traced_data.TracedRepo attribute)
traced_files_graph (lean_dojo.data_extraction.traced_data.TracedRepo attribute)
traced_repo (lean_dojo.data_extraction.traced_data.TracedFile attribute)
(lean_dojo.data_extraction.traced_data.TracedTheorem property)
traced_theorem (lean_dojo.data_extraction.traced_data.TracedTactic attribute)
TracedFile (class in lean_dojo.data_extraction.traced_data)
TracedRepo (class in lean_dojo.data_extraction.traced_data)
TracedTactic (class in lean_dojo.data_extraction.traced_data)
TracedTheorem (class in lean_dojo.data_extraction.traced_data)
trailing (lean_dojo.data_extraction.ast.AtomNode attribute)
(lean_dojo.data_extraction.ast.IdentNode attribute)
traverse_postorder() (lean_dojo.data_extraction.ast.Node method)
traverse_preorder() (lean_dojo.data_extraction.ast.Node method)
(lean_dojo.data_extraction.traced_data.TracedFile method)
U
uhash (lean_dojo.data_extraction.lean.Theorem property)
uid (lean_dojo.data_extraction.lean.Theorem property)
url (lean_dojo.data_extraction.lean.LeanGitRepo attribute)
url_to_repo() (in module lean_dojo.data_extraction.lean)
uses_commands (lean_dojo.interaction.dojo.Dojo property)
uses_tactics (lean_dojo.interaction.dojo.Dojo property)
V
val (lean_dojo.data_extraction.ast.AtomNode attribute)
(lean_dojo.data_extraction.ast.IdentNode attribute)
Read the Docs
v: latest
Versions
latest
stable
Downloads
pdf
On Read the Docs
Project Home
Builds