This API reference is generated automatically from docstrings by autodoc.
GITHUB_ACCESS_TOKEN
LEAN4_NIGHTLY_REPO
LEAN4_REPO
LeanFile
LeanGitRepo
Pos
RepoInfoCache
Theorem
cleanse_string()
get_latest_commit()
get_lean4_commit_from_config()
get_lean4_version_from_config()
is_supported_version()
normalize_url()
url_to_repo()
get_traced_repo_path()
is_available_in_cache()
trace()
Comment
TracedFile
TracedRepo
TracedTactic
TracedTheorem
get_code_without_comments()
CommandState
Dojo
DojoCrashError
DojoHardTimeoutError
DojoInitError
LeanError
ProofFinished
ProofGivenUp
TacticState
TimeoutError
Declaration
Goal
parse_goals()
CACHE_DIR
CONTAINER
DISABLE_REMOTE_CACHE
LEAN4_PACKAGES_DIR
LEAN4_URL
LOAD_USED_PACKAGES_ONLY
NUM_PROCS
REMOTE_CACHE_URL
TACTIC_CPU_LIMIT
TACTIC_MEMORY_LIMIT
TMP_DIR
check_git_version()