record_proof
flux_
infer
0.1.0
In flux_
infer::
lean_
encoding
flux_infer
::
lean_encoding
Function
record_
proof
Copy item path
Source
fn record_proof(genv:
GlobalEnv
<'_, '_>, def_id:
MaybeExternId
) ->
Result
<
()
>