Crate creusot_contracts_proc 

Macros

declare_namespace

extern_spec

ghost

ghost_let

pearlite

proof_assert

snapshot

Attribute Macros

bitwise_proof

builtin

check

ensures

erasure

intrinsic

invariant

logic

maintains

opaque

open_inv_result

requires

trusted

variant

Derive Macros

DeepModel