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.
• Default
  A trait for giving a type a useful default value.
• Eq
  Trait for comparisons corresponding to equivalence relations.
• Hash
  A hashable type.
• Hasher
  A trait for hashing an arbitrary stream of bytes.

Type Aliases

• Result
  The type returned by formatter methods.
• nat

Derive Macros

• Debug
  Derive macro generating an impl of the trait Debug.
• Default
  Derive macro generating an impl of the trait Default.
• Eq
  Derive macro generating an impl of the trait Eq.
• Hash
  Derive macro generating an impl of the trait Hash.