pub fn recheck_document(json: &str, limits: &EnvironmentLimits) -> RecheckReportExpand description
Re-check a certificate document of any kind, dispatched by its schema.
An environment certificate is rebuilt on a stack sized for its deepest term. A certificate by itself establishes that its proof checks against the environment it carries; that the statement is the Lean source’s is established by replaying the whole package, which binds it to the export.