List of all items

Structs

• AllocationTracker
• Array10
• Array11
• Array12
• Array13
• Array14
• Array15
• Array16
• Array2
• Array3
• Array4
• Array5
• Array6
• Array7
• Array8
• Array9
• DafnyChar
• DafnyCharUTF16
• DafnyInt
• DafnyPrintWrapper
• ExactPool
• FunctionWrapper
• IntegerRange
• IntegerRangeDown
• IntegerRangeDownUnbounded
• IntegerRangeUnbounded
• Lazy
• LazyFieldWrapper
• Map
• MapBuilder
• MaybePlacebo
• Multiset
• Object
• Ptr
• Rc
• RefCell
• SequenceIter
• Set
• SetBuilder
• UnsafeCell
• Weak
• _System::Formatter
• _System::Rc
• dafny_runtime_conversions::Rc
• dafny_runtime_conversions::object::Rc
• dafny_runtime_conversions::ptr::Rc
• rcmut::Array

Enums

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

Unions

• MaybeUninit

Traits

• Any
• AnyRef
• DafnyPrint
• DafnyType
• DafnyTypeEq
• DafnyUsize
• FromPrimitive
• Into
• NontrivialDefault
• NumCast
• Send
• Sync
• ToPrimitive
• Upcast
• UpcastBox
• UpcastObject
• Zero
• _System::AsRef
• _System::Debug
• _System::Eq
• _System::Hash
• _System::Hasher
• _System::PartialEq

Macros

• Extends
• INIT_ARRAY_DATA
• UpcastDef
• UpcastDefObject
• UpcastFn
• UpcastObjectFn
• _System::seq
• 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
• update_field_nodrop_object
• update_field_uninit
• update_field_uninit_object
• update_nodrop
• update_nodrop_object

Derive Macros

• _System::Debug
• _System::Eq
• _System::Hash
• _System::PartialEq

Functions

• allocate
• allocate_object
• allocate_object_track
• array::construct
• array::construct_object
• array::from_native
• array::from_vec
• array::get
• array::get_usize
• array::initialize
• array::initialize_box
• array::initialize_box_usize
• array::initialize_usize
• array::length
• array::length_usize
• array::placebos
• array::placebos_box
• array::placebos_box_usize
• array::placebos_usize
• array::placebos_usize_object
• array::to_vec
• array::update
• array::update_usize
• bigint_to_dafny_int
• box_coerce
• char_lt
• dafny_int_to_bigint
• dafny_runtime_conversions::dafny_map_to_hashmap
• dafny_runtime_conversions::dafny_multiset_to_owned_vec
• dafny_runtime_conversions::dafny_sequence_to_vec
• dafny_runtime_conversions::dafny_set_to_set
• dafny_runtime_conversions::hashmap_to_dafny_map
• dafny_runtime_conversions::object::boxed_struct_to_dafny_class
• dafny_runtime_conversions::object::dafny_array2_to_vec
• dafny_runtime_conversions::object::dafny_array_to_vec
• dafny_runtime_conversions::object::dafny_class_to_boxed_struct
• dafny_runtime_conversions::object::dafny_class_to_rc_struct
• dafny_runtime_conversions::object::dafny_class_to_struct
• dafny_runtime_conversions::object::rc_struct_to_dafny_class
• dafny_runtime_conversions::object::struct_to_dafny_class
• dafny_runtime_conversions::object::vec_to_dafny_array
• dafny_runtime_conversions::ptr::boxed_struct_to_dafny_class
• dafny_runtime_conversions::ptr::dafny_array2_to_vec
• dafny_runtime_conversions::ptr::dafny_array_to_vec
• dafny_runtime_conversions::ptr::dafny_class_to_boxed_struct
• dafny_runtime_conversions::ptr::dafny_class_to_struct
• dafny_runtime_conversions::ptr::struct_to_dafny_class
• dafny_runtime_conversions::ptr::vec_to_dafny_array
• dafny_runtime_conversions::set_to_dafny_set
• dafny_runtime_conversions::unicode_chars_false::dafny_string_to_string
• dafny_runtime_conversions::unicode_chars_false::string_to_dafny_string
• dafny_runtime_conversions::unicode_chars_true::dafny_string_to_string
• dafny_runtime_conversions::unicode_chars_true::string_to_dafny_string
• dafny_runtime_conversions::vec_to_dafny_multiset
• dafny_runtime_conversions::vec_to_dafny_sequence
• deallocate
• euclidian_division
• euclidian_modulo
• exact_range
• fn1_coerce
• integer_range
• integer_range_down
• integer_range_down_unbounded
• integer_range_unbounded
• new_field
• object::downcast
• object::is
• object::new
• rc_coerce
• rcmut::array_object_from_box
• rcmut::array_object_from_rc
• rcmut::as_rc
• rcmut::as_rc_mut
• rcmut::borrow
• rcmut::borrow_mut
• rcmut::downcast
• rcmut::from
• rcmut::from_rc
• rcmut::new
• rcmut::to_rc
• string_of
• string_utf16_of
• upcast
• upcast_box
• upcast_box_box
• upcast_id
• upcast_object

Type Aliases

• DafnyString
• DafnyStringUTF16
• DynAny
• Field
• SizeT
• _System::Result
• _System::nat
• dafny_runtime_conversions::DafnyBool
• dafny_runtime_conversions::DafnyChar
• dafny_runtime_conversions::DafnyCharUTF16
• dafny_runtime_conversions::DafnyInt
• dafny_runtime_conversions::DafnyMap
• dafny_runtime_conversions::DafnyMultiset
• dafny_runtime_conversions::DafnySequence
• dafny_runtime_conversions::DafnySet
• dafny_runtime_conversions::object::DafnyArray
• dafny_runtime_conversions::object::DafnyArray2
• dafny_runtime_conversions::object::DafnyArray3
• dafny_runtime_conversions::object::DafnyClass
• dafny_runtime_conversions::ptr::DafnyArray
• dafny_runtime_conversions::ptr::DafnyArray2
• dafny_runtime_conversions::ptr::DafnyArray3
• dafny_runtime_conversions::ptr::DafnyClass
• rcmut::RcMut