Module creusot_contracts::logic

Definitions for pearlite code

This contains types and traits that are meant to be used in logical code.

Re-exports

• pub use ord::OrdLogic;

Modules

• ops
• ord
  Definition for using orderings in pearlite.

Structs

• FMap
  A finite map type usable in pearlite and ghost! blocks.
• FSet
  A finite set type usable in pearlite and ghost! blocks.
• Int
  An unbounded, mathematical integer.
• Mapping
  A mapping: map every value of type A to a value of type B.
• Seq
  A type of sequence usable in pearlite and ghost! blocks.
• Set
  A (possibly infinite) set type.