pub fn log_proof(
genv: GlobalEnv<'_, '_>,
def_id: MaybeExternId,
) -> Result<(), ErrorGuaranteed>Expand description
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 by lake build),
regardless of whether the proof was cached.