Module lean_encoding 

Macros

string_vec 🔒

Helper macro to create Vec from string-like values

Structs

LeanEncoder

Enums

FileKind

LeanFile

Different kinds of Lean files

Functions

check_proof

constant_deps 🔒

create_file_with_dirs 🔒

Create a file at the given path, creating any missing parent directories.

create_or_truncate_file_with_dirs 🔒

Create or truncate a file at the given path, creating any missing parent directories.

final_project_path 🔒

finalize

hyperlink_proof 🔒

log_proof

We need to both hyperlink the proof (so users can easily jump to it) and record the checking file in Basic.lean (so that it gets checked by lake build), regardless of whether the proof was cached.

namespaced 🔒

project 🔒

project_path 🔒

proof_name 🔒

record_proof 🔒

rename_dir_contents 🔒

Renames all files and directories from ‘src’ to ‘dst’

run_check 🔒

run_lean 🔒

run_proof 🔒

vc_name 🔒