Modules§
- hax_
paths 🔒 - This module defines the
ImplFnDecorationstructure and utils around it.
Macros§
- coq_
expr - coq_
prop_ expr - coq_
unsafe_ expr - fstar_
expr - fstar_
prop_ expr - fstar_
unsafe_ expr - identity_
proc_ 🔒macro_ attribute - int
- loop_
decreases - loop_
invariant - proverif_
expr - proverif_
prop_ expr - proverif_
unsafe_ expr
Functions§
Attribute Macros§
- attributes
- coq_
after - coq_
before - coq_
replace - coq_
replace_ body - decreases
- ensures
- exclude
- fstar_
after - fstar_
before - fstar_
options - fstar_
postprocess_ with - fstar_
replace - fstar_
replace_ body - fstar_
smt_ pat - fstar_
verification_ status - impl_
fn_ decoration - include
- lemma
- opaque
- opaque_
type - process_
init - process_
read - process_
write - protocol_
messages - proverif_
after - proverif_
before - proverif_
replace - proverif_
replace_ body - pv_
constructor - pv_
handwritten - refinement_
type - requires
- trait_
fn_ decoration - transparent