Module lean_encoding

Module lean_encoding 

Source

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
create_file_with_dirs πŸ”’
Create a file at the given path, creating any missing parent directories.
finalize
project πŸ”’
project_path πŸ”’
rename_dir_contents πŸ”’
Renames all files and directories from β€˜src’ to β€˜dst’
run_lean πŸ”’
vc_name πŸ”’