Commit 6fd90de5 authored by Heiko Becker's avatar Heiko Becker

Add docstring to general soundness theorem

parent ab3e452e
......@@ -25,6 +25,10 @@ Definition CertificateChecker (e: expr Q) (absenv: analysisResult)
| _ => false
end.
(**
General soundness theorem, exposing all invariants that are shown by
the separate validator functions
**)
Theorem Certificate_checking_is_sound_general (e:expr Q) (absenv:analysisResult)
P Qmap subdivs defVars:
forall (E1 E2:env) DeltaMap,
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment