List of all items
Macros
- coq_expr
- coq_prop_expr
- fstar_expr
- fstar_prop_expr
- int
- legacy_lean_expr
- legacy_lean_prop_expr
- loop_decreases
- loop_invariant
- proverif_expr
- proverif_prop_expr
Attribute Macros
- attributes
- coq_after
- coq_before
- coq_replace
- coq_replace_body
- decreases
- ensures
- ensures_ref
- 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
- legacy_lean_after
- legacy_lean_before
- legacy_lean_proof
- legacy_lean_proof_method_bv_decide
- legacy_lean_proof_method_grind
- legacy_lean_pure_ensures_proof
- legacy_lean_pure_requires_proof
- legacy_lean_replace
- legacy_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