Macros§
- string_
vec 🔒 - Helper macro to create Vec
from string-like values
Structs§
Enums§
Functions§
- check_
proof - constant_
deps 🔒 - create_
file_ 🔒with_ dirs - Create a file at the given path, creating any missing parent directories.
- finalize
- hyperlink_
proof 🔒 - log_
proof - We need to both hyperlink the proof (so users can easily jump to it)
and record the proof in
Basic.lean(so that it gets checked bylake build), regardless of whether the proof was cached. - namespaced 🔒
- project 🔒
- project_
path 🔒 - record_
proof 🔒 - rename_
dir_ 🔒contents - Renames all files and directories from ‘src’ to ‘dst’
- run_
lean 🔒 - vc_name 🔒