Macros§
- coq_
expr - coq_
prop_ expr - coq_
unsafe_ expr - fstar_
expr - fstar_
prop_ expr - fstar_
unsafe_ expr - int
- lean_
expr - lean_
prop_ expr - lean_
unsafe_ expr - loop_
decreases - loop_
invariant - proverif_
expr - proverif_
prop_ expr - proverif_
unsafe_ expr
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
- lean_
after - lean_
before - lean_
replace - lean_
replace_ body - 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