lean4
lean4 copied to clipboard
refactor: lake: API cleanup / mark some defs `private`
It has long been requested to better clarify what parts of Lake API are public and which parts are internal implementation details. This change is a small step towards that by marking some definitions that should virtually never be called directly by users as private
.