Skip to main content

log_proof

flux_infer::lean_encoding

Function log_proof 

Source 
pub fn log_proof(
    genv: GlobalEnv<'_, '_>,
    def_id: MaybeExternId,
) -> Result<(), ErrorGuaranteed>
Expand description

We need to record the checking file in Basic.lean (so that it gets checked by lake build), regardless of whether the proof was cached.