Re-exports§
pub use itertools;
Modules§
Macros§
- Extends
- INIT_
ARRAY_ DATA - Upcast
Def - Upcast
DefObject - Upcast
Fn - Upcast
Object Fn - array
- cast
- cast_
any - cast_
any_ object - cast_
object - int
- is
- is_
object - map
- maybe_
placebos_ from - md
- modify
- modify_
field - multiset
- rd
- read
- read_
field - refcount
- seq
- set
- truncate
- tuple_
extract_ index - update_
field_ if_ uninit - update_
field_ if_ uninit_ object - update_
field_ mut_ if_ uninit - update_
field_ mut_ if_ uninit_ object - update_
field_ mut_ nodrop - update_
field_ mut_ nodrop_ object - update_
field_ mut_ uninit - update_
field_ mut_ uninit_ object - update_
field_ nodrop - In that case, prefer to use update_uninit
- update_
field_ nodrop_ object - update_
field_ uninit - update_
field_ uninit_ object - update_
nodrop - update_
nodrop_ object
Structs§
- Allocation
Tracker - Array2
- Array3
- Array4
- Array5
- Array6
- Array7
- Array8
- Array9
- Array10
- Array11
- Array12
- Array13
- Array14
- Array15
- Array16
- Dafny
Char - Dafny
CharUT F16 - Dafny
Int - Dafny
Print Wrapper - Exact
Pool - Function
Wrapper - Integer
Range - Integer
Range Down - Integer
Range Down Unbounded - Integer
Range Unbounded - Lazy
- A value which is initialized on the first access.
- Lazy
Field Wrapper - Map
- MapBuilder
- Maybe
Placebo - Multiset
- Object
- Ptr
- Rc
- A single-threaded reference-counting pointer. ‘Rc’ stands for ‘Reference Counted’.
- RefCell
- A mutable memory location with dynamically checked borrow rules
- Sequence
Iter - Set
- SetBuilder
- Unsafe
Cell - The core primitive for interior mutability in Rust.
- Weak
Weakis a version ofRcthat holds a non-owning reference to the managed allocation.
Enums§
Traits§
- Any
- A trait to emulate dynamic typing.
- AnyRef
- Dafny
Print - Dafny
Type - Dafny
Type Eq - Dafny
Usize - From
Primitive - A generic trait for converting a number to a value.
- Into
- A value-to-value conversion that consumes the input value. The
opposite of
From. - Nontrivial
Default - NumCast
- An interface for casting between machine scalars.
- Send
- Types that can be transferred across thread boundaries.
- Sync
- Types for which it is safe to share references between threads.
- ToPrimitive
- A generic trait for converting a value to a number.
- Upcast
- Upcast
Box - Upcast
Object - Zero
- Defines an additive identity element for
Self.
Functions§
- allocate
- allocate_
object - allocate_
object_ track - bigint_
to_ dafny_ int - box_
coerce - char_lt
- dafny_
int_ to_ bigint - deallocate
- euclidian_
division - euclidian_
modulo - exact_
range - fn1_
coerce - integer_
range - integer_
range_ down - integer_
range_ down_ unbounded - integer_
range_ unbounded - new_
field - rc_
coerce - string_
of - string_
utf16_ of - upcast
- upcast_
box - upcast_
box_ box - upcast_
id - upcast_
object
Type Aliases§
Unions§
- Maybe
Uninit - A wrapper type to construct uninitialized instances of
T.