Module _System

Re-exports§

pub use crate::DafnyInt;
pub use crate::DafnyType;
pub use crate::DafnyPrint;
pub use crate::SequenceIter;

Macros§

seq

Structs§

Formatter: Configuration for formatting.
Rc: A single-threaded reference-counting pointer. ‘Rc’ stands for ‘Reference Counted’.

Enums§

Tuple0
Tuple1
Tuple2
Tuple3
Tuple4
Tuple5
Tuple6
Tuple7
Tuple8
Tuple9
Tuple10
Tuple11
Tuple12
Tuple13
Tuple14
Tuple15
Tuple16
Tuple17
Tuple18
Tuple19
Tuple20

Traits§

AsRef: Used to do a cheap reference-to-reference conversion.
Debug: ? formatting.
Eq: Trait for comparisons corresponding to equivalence relations.
Hash: A hashable type.
Hasher: A trait for hashing an arbitrary stream of bytes.
PartialEq: Trait for comparisons using the equality operator.

Type Aliases§

Result: The type returned by formatter methods.
nat

Derive Macros§

Debug: Derive macro generating an impl of the trait Debug.
Eq: Derive macro generating an impl of the trait Eq.
Hash: Derive macro generating an impl of the trait Hash.
PartialEq: Derive macro generating an impl of the trait PartialEq. The behavior of this macro is described in detail here.