-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
-- [alloc]: function definitions
import Aeneas
import CoreModels.Core.TypesPrologue
import CoreModels.Core.Types
import CoreModels.RustPrimitives.Types
import CoreModels.Alloc.Types
import CoreModels.RustPrimitives.Funs
import CoreModels.Core.Funs
-- (alloc-side externals live in parent CoreModels.RustPrimitives)
open CoreModels Aeneas
open Aeneas.Std hiding namespace core alloc
open RustM ControlFlow Error
open Std.Do
set_option linter.dupNamespace false
set_option linter.hashCommand false
set_option linter.unusedVariables false
set_option linter.style.whitespace false
set_option linter.style.setOption false
set_option linter.style.longLine false
/- You can set the `maxHeartbeats` value with the `-max-heartbeats` CLI option -/
set_option maxHeartbeats 1000000
/- You can set the `maxRecDepth` value with the `-max-recdepth` CLI option -/
set_option maxRecDepth 2048
namespace CoreModels.alloc
/-- [alloc::alloc::{impl core::clone::Clone for alloc::alloc::Global}::clone]:
Source: 'src/lib.rs', lines 31:13-31:18
Visibility: public -/
def alloc.Global.Insts.CoreCloneClone.clone
(self : alloc.Global) : RustM alloc.Global := do
ok ()
/-- Trait implementation: [alloc::alloc::{impl core::clone::Clone for alloc::alloc::Global}]
Source: 'src/lib.rs', lines 31:13-31:18 -/
@[reducible]
impl_def alloc.Global.Insts.CoreCloneClone : core.clone.Clone alloc.Global := {
clone := alloc.Global.Insts.CoreCloneClone.clone
clone_from := core.clone.Clone.clone_from.default
alloc.Global.Insts.CoreCloneClone
}
/-- Trait implementation: [alloc::alloc::{impl alloc::alloc::Allocator for alloc::alloc::Global}]
Source: 'src/lib.rs', lines 34:4-34:32 -/
@[reducible]
def alloc.Global.Insts.AllocAllocAllocator : alloc.Allocator
alloc.Global := {
}
/-- [alloc::borrow::{impl alloc::borrow::ToOwned for T}::to_owned]:
Source: 'src/lib.rs', lines 44:8-46:9
Visibility: public -/
def borrow.ToOwned.Blanket.to_owned {T : Type} (self : T) : RustM T := do
ok self
/-- Trait implementation: [alloc::borrow::{impl alloc::borrow::ToOwned for T}]
Source: 'src/lib.rs', lines 43:4-47:5 -/
@[reducible]
def borrow.ToOwned.Blanket (T : Type) : borrow.ToOwned T := {
to_owned := borrow.ToOwned.Blanket.to_owned
}
/-- [alloc::boxed::{alloc::boxed::Box<T>}::new]:
Source: 'src/lib.rs', lines 66:8-68:9 -/
def boxed.Box.new {T : Type} (v : T) : RustM T := do
ok v
/-- [alloc::boxed::{impl core::ops::deref::Deref<T> for alloc::boxed::Box<T>}::deref]:
Source: 'src/lib.rs', lines 74:8-76:9
Visibility: public -/
def boxed.Box.Insts.CoreOpsDerefDeref.deref
{T : Type} (self : boxed.Box T) : RustM T := do
ok self
/-- Trait implementation: [alloc::boxed::{impl core::ops::deref::Deref<T> for alloc::boxed::Box<T>}]
Source: 'src/lib.rs', lines 72:4-77:5 -/
@[reducible]
def boxed.Box.Insts.CoreOpsDerefDeref (T : Type) : core.ops.deref.Deref
(boxed.Box T) T := {
deref := boxed.Box.Insts.CoreOpsDerefDeref.deref
}
/-- [alloc::boxed::{impl core::clone::Clone for alloc::boxed::Box<T>}::clone]:
Source: 'src/lib.rs', lines 81:8-83:9
Visibility: public -/
def boxed.Box.Insts.CoreCloneClone.clone
{T : Type} (corecloneCloneInst : core.clone.Clone T) (self : boxed.Box T) :
RustM (boxed.Box T)
:= do
let t ← corecloneCloneInst.clone self
ok t
/-- Trait implementation: [alloc::boxed::{impl core::clone::Clone for alloc::boxed::Box<T>}]
Source: 'src/lib.rs', lines 80:4-84:5 -/
@[reducible]
impl_def boxed.Box.Insts.CoreCloneClone {T : Type} (corecloneCloneInst :
core.clone.Clone T) : core.clone.Clone (boxed.Box T) := {
clone := boxed.Box.Insts.CoreCloneClone.clone corecloneCloneInst
clone_from := core.clone.Clone.clone_from.default
(boxed.Box.Insts.CoreCloneClone corecloneCloneInst)
}
/-- [alloc::boxed::{impl core::cmp::PartialEq<alloc::boxed::Box<U>> for alloc::boxed::Box<T>}::eq]:
Source: 'src/lib.rs', lines 96:8-98:9
Visibility: public -/
def boxed.Box.Insts.CoreCmpPartialEqBox.eq
{T : Type} {U : Type} (corecmpPartialEqInst : core.cmp.PartialEq T U)
(self : boxed.Box T) (other : boxed.Box U) :
RustM Bool
:= do
corecmpPartialEqInst.eq self other
/-- [alloc::boxed::{impl core::cmp::PartialEq<alloc::boxed::Box<U>> for alloc::boxed::Box<T>}::ne]:
Source: 'src/lib.rs', lines 93:8-95:9
Visibility: public -/
def boxed.Box.Insts.CoreCmpPartialEqBox.ne
{T : Type} {U : Type} (corecmpPartialEqInst : core.cmp.PartialEq T U)
(self : boxed.Box T) (other : boxed.Box U) :
RustM Bool
:= do
let b ←
boxed.Box.Insts.CoreCmpPartialEqBox.eq corecmpPartialEqInst self other
ok (b = false)
/-- Trait implementation: [alloc::boxed::{impl core::cmp::PartialEq<alloc::boxed::Box<U>> for alloc::boxed::Box<T>}]
Source: 'src/lib.rs', lines 91:4-99:5 -/
@[reducible]
def boxed.Box.Insts.CoreCmpPartialEqBox {T : Type} {U : Type}
(corecmpPartialEqInst : core.cmp.PartialEq T U) : core.cmp.PartialEq
(boxed.Box T) (boxed.Box U) := {
eq := boxed.Box.Insts.CoreCmpPartialEqBox.eq corecmpPartialEqInst
ne := boxed.Box.Insts.CoreCmpPartialEqBox.ne corecmpPartialEqInst
}
/-- [alloc::collections::btree::set::{alloc::collections::btree::set::BTreeSet<T, U>}::new]:
Source: 'src/lib.rs', lines 296:16-298:17 -/
def collections.btree.set.BTreeSet.new
(T : Type) (U : Type) : RustM (collections.btree.set.BTreeSet T U) := do
ok (core.option.Option.None, core.option.Option.None)
/-- [alloc::collections::vec_deque::{alloc::collections::vec_deque::VecDeque<T, alloc::alloc::Global>}::new]:
Source: 'src/lib.rs', lines 312:12-314:13 -/
def collections.vec_deque.VecDequeTGlobal.new
(T : Type) : RustM (collections.vec_deque.VecDeque T alloc.Global) := do
let s ← rust_primitives.sequence.seq_empty T
ok (s, core.marker.PhantomData.mk)
/-- [alloc::collections::vec_deque::{alloc::collections::vec_deque::VecDeque<T, alloc::alloc::Global>}::with_capacity]:
Source: 'src/lib.rs', lines 315:12-317:13 -/
def collections.vec_deque.VecDequeTGlobal.with_capacity
(T : Type) (_capacity : Std.Usize) :
RustM (collections.vec_deque.VecDeque T alloc.Global)
:= do
collections.vec_deque.VecDequeTGlobal.new T
/-- [alloc::collections::vec_deque::{alloc::collections::vec_deque::VecDeque<T, A>}::push_back]:
Source: 'src/lib.rs', lines 323:12-325:13 -/
def collections.vec_deque.VecDeque.push_back
{T : Type} {A : Type} (self : collections.vec_deque.VecDeque T A) (x : T) :
RustM (collections.vec_deque.VecDeque T A)
:= do
let (s, pd) := self
let s1 ← rust_primitives.sequence.seq_push s x
ok (s1, pd)
/-- [alloc::collections::vec_deque::{alloc::collections::vec_deque::VecDeque<T, A>}::len]:
Source: 'src/lib.rs', lines 326:12-328:13 -/
def collections.vec_deque.VecDeque.len
{T : Type} {A : Type} (self : collections.vec_deque.VecDeque T A) :
RustM Std.Usize
:= do
let (s, _) := self
rust_primitives.sequence.seq_len s
/-- [alloc::collections::vec_deque::{alloc::collections::vec_deque::VecDeque<T, A>}::pop_front]:
Source: 'src/lib.rs', lines 329:12-335:13 -/
def collections.vec_deque.VecDeque.pop_front
{T : Type} {A : Type} (self : collections.vec_deque.VecDeque T A) :
RustM ((core.option.Option T) × (collections.vec_deque.VecDeque T A))
:= do
let i ← collections.vec_deque.VecDeque.len self
if i = 0#usize
then ok (core.option.Option.None, self)
else
let (s, pd) := self
let (t, s1) ← rust_primitives.sequence.seq_remove s 0#usize
ok (core.option.Option.Some t, (s1, pd))
/-- [alloc::collections::vec_deque::{impl core::ops::index::Index<usize, T> for alloc::collections::vec_deque::VecDeque<T, A>}::index]:
Source: 'src/lib.rs', lines 342:12-344:13
Visibility: public -/
def collections.vec_deque.VecDeque.Insts.CoreOpsIndexIndexUsizeT.index
{T : Type} {A : Type} (self : collections.vec_deque.VecDeque T A)
(i : Std.Usize) :
RustM T
:= do
let (s, _) := self
rust_primitives.sequence.seq_index s i
/-- Trait implementation: [alloc::collections::vec_deque::{impl core::ops::index::Index<usize, T> for alloc::collections::vec_deque::VecDeque<T, A>}]
Source: 'src/lib.rs', lines 339:8-345:9 -/
@[reducible]
def collections.vec_deque.VecDeque.Insts.CoreOpsIndexIndexUsizeT (T : Type) (A
: Type) : core.ops.index.Index (collections.vec_deque.VecDeque T A) Std.Usize
T := {
index := collections.vec_deque.VecDeque.Insts.CoreOpsIndexIndexUsizeT.index
}
/-- [alloc::collections::vec_deque::into_iter::{impl core::iter::traits::iterator::Iterator<T> for alloc::collections::vec_deque::into_iter::IntoIter<T, A>}::next]:
Source: 'src/lib.rs', lines 352:16-358:17
Visibility: public -/
def
collections.vec_deque.into_iter.IntoIter.Insts.CoreIterTraitsIteratorIterator.next
{T : Type} {A : Type} (self : collections.vec_deque.into_iter.IntoIter T A) :
RustM ((core.option.Option T) × (collections.vec_deque.into_iter.IntoIter T
A))
:= do
let (s, pd) := self
let i ← rust_primitives.sequence.seq_len s
if i = 0#usize
then ok (core.option.Option.None, self)
else
let (t, s1) ← rust_primitives.sequence.seq_remove s 0#usize
ok (core.option.Option.Some t, (s1, pd))
/-- Trait implementation: [alloc::collections::vec_deque::into_iter::{impl core::iter::traits::iterator::Iterator<T> for alloc::collections::vec_deque::into_iter::IntoIter<T, A>}]
Source: 'src/lib.rs', lines 350:12-359:13 -/
@[reducible]
def
collections.vec_deque.into_iter.IntoIter.Insts.CoreIterTraitsIteratorIterator
(T : Type) (A : Type) : core.iter.traits.iterator.Iterator
(collections.vec_deque.into_iter.IntoIter T A) T := {
next :=
collections.vec_deque.into_iter.IntoIter.Insts.CoreIterTraitsIteratorIterator.next
}
/-- [alloc::collections::vec_deque::{impl core::iter::traits::collect::IntoIterator<T, alloc::collections::vec_deque::into_iter::IntoIter<T, A>> for alloc::collections::vec_deque::VecDeque<T, A>}::into_iter]:
Source: 'src/lib.rs', lines 366:12-368:13
Visibility: public -/
def
collections.vec_deque.VecDeque.Insts.CoreIterTraitsCollectIntoIteratorTIntoIter.into_iter
{T : Type} {A : Type} (self : collections.vec_deque.VecDeque T A) :
RustM (collections.vec_deque.into_iter.IntoIter T A)
:= do
let (s, _) := self
ok (s, core.marker.PhantomData.mk)
/-- Trait implementation: [alloc::collections::vec_deque::{impl core::iter::traits::collect::IntoIterator<T, alloc::collections::vec_deque::into_iter::IntoIter<T, A>> for alloc::collections::vec_deque::VecDeque<T, A>}]
Source: 'src/lib.rs', lines 363:8-369:9 -/
@[reducible]
def
collections.vec_deque.VecDeque.Insts.CoreIterTraitsCollectIntoIteratorTIntoIter
(T : Type) (A : Type) : core.iter.traits.collect.IntoIterator
(collections.vec_deque.VecDeque T A) T
(collections.vec_deque.into_iter.IntoIter T A) := {
iteratorIteratorInst :=
collections.vec_deque.into_iter.IntoIter.Insts.CoreIterTraitsIteratorIterator
T A
into_iter :=
collections.vec_deque.VecDeque.Insts.CoreIterTraitsCollectIntoIteratorTIntoIter.into_iter
}
/-- [alloc::vec::from_seq]:
Source: 'src/lib.rs', lines 729:4-731:5 -/
def vec.from_seq
{T : Type} (s : rust_primitives.sequence.Seq T) : RustM (vec.Vec T) := do
ok s
/-- [alloc::slice::{alloc::slice::Dummy<T>}::to_vec]:
Source: 'src/lib.rs', lines 514:8-521:9 -/
def slice.Dummy.to_vec
{T : Type} (corecloneCloneInst : core.clone.Clone T) (s : Slice T) :
RustM (vec.Vec T)
:= do
let seq ← rust_primitives.sequence.seq_empty T
let seq1 ← rust_primitives.sequence.seq_extend corecloneCloneInst seq s
vec.from_seq seq1
/-- [alloc::slice::{alloc::slice::Dummy<T>}::into_vec]:
Source: 'src/lib.rs', lines 523:8-525:9 -/
def slice.Dummy.into_vec {T : Type} (s : Slice T) : RustM (vec.Vec T) := do
let s1 ← rust_primitives.sequence.seq_from_boxed_slice s
vec.from_seq s1
/-- [alloc::slice::{alloc::slice::Dummy<T>}::concat]: loop body 0:
Source: 'src/lib.rs', lines 538:12-541:13 -/
@[rust_loop_body]
def slice.Dummy.concat_loop.body
{T : Type} {Item : Type} (corecloneCloneInst : core.clone.Clone Item)
(coreborrowBorrowTSliceInst : core.borrow.Borrow T (Slice Item))
(s : Slice T) (out : rust_primitives.sequence.Seq Item) (i : Std.Usize) :
RustM (ControlFlow ((rust_primitives.sequence.Seq Item) × Std.Usize)
(rust_primitives.sequence.Seq Item))
:= do
let i1 ← rust_primitives.slice.slice_length s
if i < i1
then
let t ← rust_primitives.slice.slice_index s i
let s1 ← coreborrowBorrowTSliceInst.borrow t
let out1 ← rust_primitives.sequence.seq_extend corecloneCloneInst out s1
let i2 ← i + 1#usize
ok (cont (out1, i2))
else ok (done out)
/-- [alloc::slice::{alloc::slice::Dummy<T>}::concat]: loop 0:
Source: 'src/lib.rs', lines 538:12-541:13 -/
@[rust_loop]
def slice.Dummy.concat_loop
{T : Type} {Item : Type} (corecloneCloneInst : core.clone.Clone Item)
(coreborrowBorrowTSliceInst : core.borrow.Borrow T (Slice Item))
(s : Slice T) (out : rust_primitives.sequence.Seq Item) (i : Std.Usize) :
RustM (rust_primitives.sequence.Seq Item)
:= do
loop
(fun (out1, i1) => slice.Dummy.concat_loop.body corecloneCloneInst
coreborrowBorrowTSliceInst s out1 i1)
(out, i)
/-- [alloc::slice::{alloc::slice::Dummy<T>}::concat]:
Source: 'src/lib.rs', lines 532:8-543:9 -/
def slice.Dummy.concat
{T : Type} {Item : Type} (corecloneCloneInst : core.clone.Clone Item)
(coreborrowBorrowTSliceInst : core.borrow.Borrow T (Slice Item))
(s : Slice T) :
RustM (vec.Vec Item)
:= do
let out ← rust_primitives.sequence.seq_empty Item
let out1 ←
slice.Dummy.concat_loop corecloneCloneInst coreborrowBorrowTSliceInst s out
0#usize
vec.from_seq out1
/-- [alloc::vec::{alloc::vec::Vec<T>}::as_slice]:
Source: 'src/lib.rs', lines 844:8-846:9
Visibility: public -/
def vec.Vec.as_slice {T : Type} (self : vec.Vec T) : RustM (Slice T) := do
rust_primitives.sequence.seq_to_slice self
/-- [alloc::vec::{impl core::ops::deref::Deref<[T]> for alloc::vec::Vec<T>}::deref]:
Source: 'src/lib.rs', lines 997:8-999:9
Visibility: public -/
def vec.Vec.Insts.CoreOpsDerefDerefSlice.deref
{T : Type} (self : vec.Vec T) : RustM (Slice T) := do
vec.Vec.as_slice self
/-- [alloc::vec::{impl core::clone::Clone for alloc::vec::Vec<T>}::clone]: loop body 0:
Source: 'src/lib.rs', lines 736:12-738:13
Visibility: public -/
@[rust_loop_body]
def vec.Vec.Insts.CoreCloneClone.clone_loop.body
{T : Type} (corecloneCloneInst : core.clone.Clone T)
(iter_ : core.slice.iter.Iter T) (new_vec : rust_primitives.sequence.Seq T) :
RustM (ControlFlow ((core.slice.iter.Iter T) × (rust_primitives.sequence.Seq
T)) (rust_primitives.sequence.Seq T))
:= do
let (o, iter1) ←
core.slice.iter.Iter.Insts.CoreIterTraitsIteratorIteratorSharedAT.next iter_
match o with
| core.option.Option.None => ok (done new_vec)
| core.option.Option.Some it =>
let t ← corecloneCloneInst.clone it
let new_vec1 ← rust_primitives.sequence.seq_push new_vec t
ok (cont (iter1, new_vec1))
/-- [alloc::vec::{impl core::clone::Clone for alloc::vec::Vec<T>}::clone]: loop 0:
Source: 'src/lib.rs', lines 736:12-738:13
Visibility: public -/
@[rust_loop]
def vec.Vec.Insts.CoreCloneClone.clone_loop
{T : Type} (corecloneCloneInst : core.clone.Clone T)
(iter_ : core.slice.iter.Iter T) (new_vec : rust_primitives.sequence.Seq T) :
RustM (rust_primitives.sequence.Seq T)
:= do
loop
(fun (iter1, new_vec1) => vec.Vec.Insts.CoreCloneClone.clone_loop.body
corecloneCloneInst iter1 new_vec1)
(iter_, new_vec)
/-- [alloc::vec::{impl core::clone::Clone for alloc::vec::Vec<T>}::clone]:
Source: 'src/lib.rs', lines 734:8-740:9
Visibility: public -/
def vec.Vec.Insts.CoreCloneClone.clone
{T : Type} (corecloneCloneInst : core.clone.Clone T) (self : vec.Vec T) :
RustM (vec.Vec T)
:= do
let new_vec ← rust_primitives.sequence.seq_empty T
let s ← vec.Vec.Insts.CoreOpsDerefDerefSlice.deref self
let iter ← core.slice.Slice.iter s
let new_vec1 ←
vec.Vec.Insts.CoreCloneClone.clone_loop corecloneCloneInst iter new_vec
ok new_vec1
/-- Trait implementation: [alloc::vec::{impl core::clone::Clone for alloc::vec::Vec<T>}]
Source: 'src/lib.rs', lines 733:4-741:5 -/
@[reducible]
impl_def vec.Vec.Insts.CoreCloneClone {T : Type} (corecloneCloneInst :
core.clone.Clone T) : core.clone.Clone (vec.Vec T) := {
clone := vec.Vec.Insts.CoreCloneClone.clone corecloneCloneInst
clone_from := core.clone.Clone.clone_from.default
(vec.Vec.Insts.CoreCloneClone corecloneCloneInst)
}
/-- [alloc::vec::{impl core::ops::index::Index<I, Clause0_Output> for alloc::vec::Vec<T>}::index]:
Source: 'src/lib.rs', lines 972:8-974:9
Visibility: public -/
def vec.Vec.Insts.CoreOpsIndexIndex.index
{T : Type} {I : Type} {Clause0_Output : Type}
(coresliceindexSliceIndexISliceClause0_OutputInst :
core.slice.index.SliceIndex I (Slice T) Clause0_Output) (self : vec.Vec T)
(i : I) :
RustM Clause0_Output
:= do
let s ← vec.Vec.Insts.CoreOpsDerefDerefSlice.deref self
core.Slice.Insts.CoreOpsIndexIndex.index
coresliceindexSliceIndexISliceClause0_OutputInst s i
/-- [alloc::vec::{alloc::vec::Vec<T>}::len]:
Source: 'src/lib.rs', lines 818:8-820:9
Visibility: public -/
def vec.Vec.len {T : Type} (self : vec.Vec T) : RustM Std.Usize := do
rust_primitives.sequence.seq_len self
/-- [alloc::vec::{impl core::cmp::PartialEq<alloc::vec::Vec<U>> for alloc::vec::Vec<T>}::eq]: loop body 0:
Source: 'src/lib.rs', lines 1:0-762:17
Visibility: public -/
@[rust_loop_body]
def vec.Vec.Insts.CoreCmpPartialEqVec.eq_loop.body
{T : Type} {U : Type} (corecmpPartialEqInst : core.cmp.PartialEq T U)
(self : vec.Vec T) (other : vec.Vec U)
(iter_ : core.ops.range.Range Std.Usize) (res : Bool) :
RustM (ControlFlow ((core.ops.range.Range Std.Usize) × Bool) Bool)
:= do
let (o, iter1) ←
core.ops.range.Range.Insts.CoreIterTraitsIteratorIterator.next
core.Usize.Insts.CoreIterRangeStep iter_
match o with
| core.option.Option.None => ok (done res)
| core.option.Option.Some i =>
if res
then
let t ←
vec.Vec.Insts.CoreOpsIndexIndex.index
(core.Usize.Insts.CoreSliceIndexSliceIndexSliceT T) self i
let t1 ←
vec.Vec.Insts.CoreOpsIndexIndex.index
(core.Usize.Insts.CoreSliceIndexSliceIndexSliceT U) other i
let b ← corecmpPartialEqInst.eq t t1
if b
then ok (cont (iter1, true))
else ok (cont (iter1, false))
else ok (cont (iter1, false))
/-- [alloc::vec::{impl core::cmp::PartialEq<alloc::vec::Vec<U>> for alloc::vec::Vec<T>}::eq]: loop 0:
Source: 'src/lib.rs', lines 1:0-762:17
Visibility: public -/
@[rust_loop]
def vec.Vec.Insts.CoreCmpPartialEqVec.eq_loop
{T : Type} {U : Type} (corecmpPartialEqInst : core.cmp.PartialEq T U)
(iter_ : core.ops.range.Range Std.Usize) (self : vec.Vec T)
(other : vec.Vec U) (res : Bool) :
RustM Bool
:= do
loop
(fun (iter1, res1) => vec.Vec.Insts.CoreCmpPartialEqVec.eq_loop.body
corecmpPartialEqInst self other iter1 res1)
(iter_, res)
/-- [alloc::vec::{impl core::cmp::PartialEq<alloc::vec::Vec<U>> for alloc::vec::Vec<T>}::eq]:
Source: 'src/lib.rs', lines 750:8-765:9
Visibility: public -/
def vec.Vec.Insts.CoreCmpPartialEqVec.eq
{T : Type} {U : Type} (corecmpPartialEqInst : core.cmp.PartialEq T U)
(self : vec.Vec T) (other : vec.Vec U) :
RustM Bool
:= do
let i ← vec.Vec.len self
let i1 ← vec.Vec.len other
if i = i1
then
vec.Vec.Insts.CoreCmpPartialEqVec.eq_loop corecmpPartialEqInst
{ start := 0#usize, «end» := i } self other true
else ok false
/-- [alloc::vec::{impl core::cmp::PartialEq<alloc::vec::Vec<U>> for alloc::vec::Vec<T>}::ne]:
Source: 'src/lib.rs', lines 747:8-749:9
Visibility: public -/
def vec.Vec.Insts.CoreCmpPartialEqVec.ne
{T : Type} {U : Type} (corecmpPartialEqInst : core.cmp.PartialEq T U)
(self : vec.Vec T) (other : vec.Vec U) :
RustM Bool
:= do
let b ←
vec.Vec.Insts.CoreCmpPartialEqVec.eq corecmpPartialEqInst self other
ok (b = false)
/-- Trait implementation: [alloc::vec::{impl core::cmp::PartialEq<alloc::vec::Vec<U>> for alloc::vec::Vec<T>}]
Source: 'src/lib.rs', lines 742:4-766:5 -/
@[reducible]
def vec.Vec.Insts.CoreCmpPartialEqVec {T : Type} {U : Type}
(corecmpPartialEqInst : core.cmp.PartialEq T U) : core.cmp.PartialEq (vec.Vec
T) (vec.Vec U) := {
eq := vec.Vec.Insts.CoreCmpPartialEqVec.eq corecmpPartialEqInst
ne := vec.Vec.Insts.CoreCmpPartialEqVec.ne corecmpPartialEqInst
}
/-- [alloc::vec::into_iter::{impl core::iter::traits::iterator::Iterator<T> for alloc::vec::into_iter::IntoIter<T>}::next]:
Source: 'src/lib.rs', lines 777:12-783:13
Visibility: public -/
def vec.into_iter.IntoIter.Insts.CoreIterTraitsIteratorIterator.next
{T : Type} (self : vec.into_iter.IntoIter T) :
RustM ((core.option.Option T) × (vec.into_iter.IntoIter T))
:= do
let i ← rust_primitives.sequence.seq_len self
if i = 0#usize
then ok (core.option.Option.None, self)
else
let (t, s) ← rust_primitives.sequence.seq_remove self 0#usize
ok (core.option.Option.Some t, s)
/-- Trait implementation: [alloc::vec::into_iter::{impl core::iter::traits::iterator::Iterator<T> for alloc::vec::into_iter::IntoIter<T>}]
Source: 'src/lib.rs', lines 775:8-784:9 -/
@[reducible]
def vec.into_iter.IntoIter.Insts.CoreIterTraitsIteratorIterator (T : Type) :
core.iter.traits.iterator.Iterator (vec.into_iter.IntoIter T) T := {
next := vec.into_iter.IntoIter.Insts.CoreIterTraitsIteratorIterator.next
}
/-- [alloc::vec::{impl core::iter::traits::collect::IntoIterator<T, alloc::vec::into_iter::IntoIter<T>> for alloc::vec::Vec<T>}::into_iter]:
Source: 'src/lib.rs', lines 790:8-792:9
Visibility: public -/
def vec.Vec.Insts.CoreIterTraitsCollectIntoIteratorTIntoIter.into_iter
{T : Type} (self : vec.Vec T) : RustM (vec.into_iter.IntoIter T) := do
ok self
/-- Trait implementation: [alloc::vec::{impl core::iter::traits::collect::IntoIterator<T, alloc::vec::into_iter::IntoIter<T>> for alloc::vec::Vec<T>}]
Source: 'src/lib.rs', lines 787:4-793:5 -/
@[reducible]
def vec.Vec.Insts.CoreIterTraitsCollectIntoIteratorTIntoIter (T : Type) :
core.iter.traits.collect.IntoIterator (vec.Vec T) T (vec.into_iter.IntoIter
T) := {
iteratorIteratorInst :=
vec.into_iter.IntoIter.Insts.CoreIterTraitsIteratorIterator T
into_iter :=
vec.Vec.Insts.CoreIterTraitsCollectIntoIteratorTIntoIter.into_iter
}
/-- [alloc::vec::from_elem]:
Source: 'src/lib.rs', lines 795:4-797:5 -/
def vec.from_elem
{T : Type} (corecloneCloneInst : core.clone.Clone T) (item : T)
(len : Std.Usize) :
RustM (vec.Vec T)
:= do
let s ← rust_primitives.sequence.seq_create corecloneCloneInst item len
ok s
/-- [alloc::vec::{alloc::vec::Vec<T>}::new]:
Source: 'src/lib.rs', lines 801:8-803:9
Visibility: public -/
def vec.Vec.new (T : Type) : RustM (vec.Vec T) := do
let s ← rust_primitives.sequence.seq_empty T
ok s
/-- [alloc::vec::{alloc::vec::Vec<T>}::with_capacity]:
Source: 'src/lib.rs', lines 804:8-806:9
Visibility: public -/
def vec.Vec.with_capacity (T : Type) (_c : Std.Usize) : RustM (vec.Vec T) := do
vec.Vec.new T
/-- [alloc::vec::{impl core::default::Default for alloc::vec::Vec<T>}::default]:
Source: 'src/lib.rs', lines 811:8-813:9
Visibility: public -/
def vec.Vec.Insts.CoreDefaultDefault.default
(T : Type) : RustM (vec.Vec T) := do
vec.Vec.new T
/-- Trait implementation: [alloc::vec::{impl core::default::Default for alloc::vec::Vec<T>}]
Source: 'src/lib.rs', lines 810:4-814:5 -/
@[reducible]
def vec.Vec.Insts.CoreDefaultDefault (T : Type) : core.default.Default (vec.Vec
T) := {
default := vec.Vec.Insts.CoreDefaultDefault.default T
}
/-- [alloc::vec::{alloc::vec::Vec<T>}::push]:
Source: 'src/lib.rs', lines 822:8-824:9
Visibility: public -/
def vec.Vec.push
{T : Type} (self : vec.Vec T) (x : T) : RustM (vec.Vec T) := do
let s ← rust_primitives.sequence.seq_push self x
ok s
/-- [alloc::vec::{alloc::vec::Vec<T>}::pop]:
Source: 'src/lib.rs', lines 825:8-833:9
Visibility: public -/
def vec.Vec.pop
{T : Type} (self : vec.Vec T) :
RustM ((core.option.Option T) × (vec.Vec T))
:= do
let l ← rust_primitives.sequence.seq_len self
if l > 0#usize
then
let i ← l - 1#usize
let (last, s) ← rust_primitives.sequence.seq_remove self i
ok (core.option.Option.Some last, s)
else ok (core.option.Option.None, self)
/-- [alloc::vec::{alloc::vec::Vec<T>}::is_empty]:
Source: 'src/lib.rs', lines 834:8-836:9
Visibility: public -/
def vec.Vec.is_empty {T : Type} (self : vec.Vec T) : RustM Bool := do
let i ← rust_primitives.sequence.seq_len self
ok (i = 0#usize)
/-- [alloc::vec::{alloc::vec::Vec<T>}::insert]:
Source: 'src/lib.rs', lines 838:8-843:9
Visibility: public -/
def vec.Vec.insert
{T : Type} (self : vec.Vec T) (index : Std.Usize) (element : T) :
RustM (vec.Vec T)
:= do
let l ← rust_primitives.sequence.seq_len self
let (right, s) ← rust_primitives.sequence.seq_drain self index l
let s1 ← rust_primitives.sequence.seq_push s element
let (s2, _) ← rust_primitives.sequence.seq_concat s1 right
ok s2
/-- [alloc::vec::{alloc::vec::Vec<T>}::as_mut_slice]:
Source: 'src/lib.rs', lines 850:8-852:9
Visibility: public -/
def vec.Vec.as_mut_slice
{T : Type} (self : vec.Vec T) :
RustM ((Slice T) × (Slice T → vec.Vec T))
:= do
let (s, seq_to_slice_mut_back) ←
rust_primitives.sequence.seq_to_slice_mut self
let back := fun s1 => let s2 := seq_to_slice_mut_back s1
s2
ok (s, back)
/-- [alloc::vec::{alloc::vec::Vec<T>}::truncate]:
Source: 'src/lib.rs', lines 856:8-861:9
Visibility: public -/
def vec.Vec.truncate
{T : Type} (self : vec.Vec T) (n : Std.Usize) : RustM (vec.Vec T) := do
let l ← rust_primitives.sequence.seq_len self
if n < l
then let (_, s) ← rust_primitives.sequence.seq_drain self n l
ok s
else ok self
/-- [alloc::vec::{alloc::vec::Vec<T>}::swap_remove]:
Source: 'src/lib.rs', lines 864:8-874:9
Visibility: public -/
def vec.Vec.swap_remove
{T : Type} (self : vec.Vec T) (n : Std.Usize) :
RustM (T × (vec.Vec T))
:= do
let l ← rust_primitives.sequence.seq_len self
let i ← l - 1#usize
let (last, s) ← rust_primitives.sequence.seq_remove self i
if n = i
then ok (last, s)
else
let (removed, s1) ← rust_primitives.sequence.seq_remove s n
let self1 ← vec.Vec.insert s1 n last
ok (removed, self1)
/-- [alloc::vec::{alloc::vec::Vec<T>}::remove]:
Source: 'src/lib.rs', lines 881:8-883:9
Visibility: public -/
def vec.Vec.remove
{T : Type} (self : vec.Vec T) (index : Std.Usize) :
RustM (T × (vec.Vec T))
:= do
let (t, s) ← rust_primitives.sequence.seq_remove self index
ok (t, s)
/-- [alloc::vec::{alloc::vec::Vec<T>}::clear]:
Source: 'src/lib.rs', lines 885:8-887:9
Visibility: public -/
def vec.Vec.clear {T : Type} (self : vec.Vec T) : RustM (vec.Vec T) := do
let s ← rust_primitives.sequence.seq_empty T
ok s
/-- [alloc::vec::{alloc::vec::Vec<T>}::append]:
Source: 'src/lib.rs', lines 889:8-892:9
Visibility: public -/
def vec.Vec.append
{T : Type} (self : vec.Vec T) (other : vec.Vec T) :
RustM ((vec.Vec T) × (vec.Vec T))
:= do
let (s, _) ← rust_primitives.sequence.seq_concat self other
let s1 ← rust_primitives.sequence.seq_empty T
ok (s, s1)
/-- [alloc::vec::{alloc::vec::Vec<T>}::split_off]:
Source: 'src/lib.rs', lines 896:8-899:9
Visibility: public -/
def vec.Vec.split_off
{T : Type} (self : vec.Vec T) («at» : Std.Usize) :
RustM ((vec.Vec T) × (vec.Vec T))
:= do
let l ← rust_primitives.sequence.seq_len self
let (s, s1) ← rust_primitives.sequence.seq_drain self «at» l
ok (s, s1)
/-- [alloc::vec::drain::{impl core::iter::traits::iterator::Iterator<T> for alloc::vec::drain::Drain<T, A>}::next]:
Source: 'src/lib.rs', lines 917:12-924:13
Visibility: public -/
def vec.drain.Drain.Insts.CoreIterTraitsIteratorIterator.next
{T : Type} {A : Type} (self : vec.drain.Drain T A) :
RustM ((core.option.Option T) × (vec.drain.Drain T A))
:= do
let (s, pd) := self
let i ← rust_primitives.sequence.seq_len s
if i = 0#usize
then ok (core.option.Option.None, self)
else
let (res, s1) ← rust_primitives.sequence.seq_remove s 0#usize
ok (core.option.Option.Some res, (s1, pd))
/-- Trait implementation: [alloc::vec::drain::{impl core::iter::traits::iterator::Iterator<T> for alloc::vec::drain::Drain<T, A>}]
Source: 'src/lib.rs', lines 915:8-925:9 -/
@[reducible]
def vec.drain.Drain.Insts.CoreIterTraitsIteratorIterator (T : Type) (A : Type)
: core.iter.traits.iterator.Iterator (vec.drain.Drain T A) T := {
next := vec.drain.Drain.Insts.CoreIterTraitsIteratorIterator.next
}
/-- [alloc::vec::{alloc::vec::Vec<T>}::extend_from_slice]:
Source: 'src/lib.rs', lines 935:8-937:9 -/
def vec.Vec.extend_from_slice
{T : Type} (corecloneCloneInst : core.clone.Clone T) (self : vec.Vec T)
(other : Slice T) :
RustM (vec.Vec T)
:= do
let s ← rust_primitives.sequence.seq_extend corecloneCloneInst self other
ok s
/-- [alloc::vec::{alloc::vec::Vec<T>}::resize]:
Source: 'src/lib.rs', lines 942:8-950:9
Visibility: public -/
def vec.Vec.resize
{T : Type} (corecloneCloneInst : core.clone.Clone T) (self : vec.Vec T)
(new_size : Std.Usize) (value : T) :
RustM (vec.Vec T)
:= do
let l ← rust_primitives.sequence.seq_len self
if new_size > l
then
let i ← new_size - l
let extra ←
rust_primitives.sequence.seq_create corecloneCloneInst value i
let (s, _) ← rust_primitives.sequence.seq_concat self extra
ok s
else let (_, s) ← rust_primitives.sequence.seq_drain self new_size l
ok s
/-- Trait implementation: [alloc::vec::{impl core::ops::index::Index<I, Clause0_Output> for alloc::vec::Vec<T>}]
Source: 'src/lib.rs', lines 966:4-975:5 -/
@[reducible]
def vec.Vec.Insts.CoreOpsIndexIndex {T : Type} {I : Type} {Clause0_Output :
Type} (coresliceindexSliceIndexISliceClause0_OutputInst :
core.slice.index.SliceIndex I (Slice T) Clause0_Output) :
core.ops.index.Index (vec.Vec T) I Clause0_Output := {
index := vec.Vec.Insts.CoreOpsIndexIndex.index
coresliceindexSliceIndexISliceClause0_OutputInst
}
/-- [alloc::vec::{impl core::ops::index::IndexMut<I, Clause0_Output> for alloc::vec::Vec<T>}::index_mut]:
Source: 'src/lib.rs', lines 988:8-990:9
Visibility: public -/
def vec.Vec.Insts.CoreOpsIndexIndexMut.index_mut
{T : Type} {I : Type} {Clause0_Output : Type}
(coresliceindexSliceIndexISliceClause0_OutputInst :
core.slice.index.SliceIndex I (Slice T) Clause0_Output) (self : vec.Vec T)
(i : I) :
RustM (Clause0_Output × (Clause0_Output → vec.Vec T))
:= do
let (s, seq_to_slice_mut_back) ←
rust_primitives.sequence.seq_to_slice_mut self
let (t, index_mut_back) ←
core.Slice.Insts.CoreOpsIndexIndexMut.index_mut
coresliceindexSliceIndexISliceClause0_OutputInst s i
let back :=
fun t1 => let s1 := index_mut_back t1
let s2 := seq_to_slice_mut_back s1
s2
ok (t, back)
/-- Trait implementation: [alloc::vec::{impl core::ops::index::IndexMut<I, Clause0_Output> for alloc::vec::Vec<T>}]
Source: 'src/lib.rs', lines 982:4-991:5 -/
@[reducible]
def vec.Vec.Insts.CoreOpsIndexIndexMut {T : Type} {I : Type} {Clause0_Output :
Type} (coresliceindexSliceIndexISliceClause0_OutputInst :
core.slice.index.SliceIndex I (Slice T) Clause0_Output) :
core.ops.index.IndexMut (vec.Vec T) I Clause0_Output := {
IndexInst := vec.Vec.Insts.CoreOpsIndexIndex
coresliceindexSliceIndexISliceClause0_OutputInst
index_mut := vec.Vec.Insts.CoreOpsIndexIndexMut.index_mut
coresliceindexSliceIndexISliceClause0_OutputInst
}
/-- Trait implementation: [alloc::vec::{impl core::ops::deref::Deref<[T]> for alloc::vec::Vec<T>}]
Source: 'src/lib.rs', lines 994:4-1000:5 -/
@[reducible]
def vec.Vec.Insts.CoreOpsDerefDerefSlice (T : Type) : core.ops.deref.Deref
(vec.Vec T) (Slice T) := {
deref := vec.Vec.Insts.CoreOpsDerefDerefSlice.deref
}
/-- [alloc::vec::{impl core::ops::deref::DerefMut<[T]> for alloc::vec::Vec<T>}::deref_mut]:
Source: 'src/lib.rs', lines 1007:8-1009:9
Visibility: public -/
def vec.Vec.Insts.CoreOpsDerefDerefMutSlice.deref_mut
{T : Type} (self : vec.Vec T) :
RustM ((Slice T) × (Slice T → vec.Vec T))
:= do
vec.Vec.as_mut_slice self
/-- Trait implementation: [alloc::vec::{impl core::ops::deref::DerefMut<[T]> for alloc::vec::Vec<T>}]
Source: 'src/lib.rs', lines 1006:4-1010:5 -/
@[reducible]
def vec.Vec.Insts.CoreOpsDerefDerefMutSlice (T : Type) :
core.ops.deref.DerefMut (vec.Vec T) (Slice T) := {
DerefInst := vec.Vec.Insts.CoreOpsDerefDerefSlice T
deref_mut := vec.Vec.Insts.CoreOpsDerefDerefMutSlice.deref_mut
}
/-- [alloc::vec::{impl core::convert::From<[T; N]> for alloc::vec::Vec<T>}::from]:
Source: 'src/lib.rs', lines 1014:8-1016:9
Visibility: public -/
def vec.Vec.Insts.CoreConvertFromArray.from
{T : Type} {N : Std.Usize} (a : Array T N) : RustM (vec.Vec T) := do
let s ← rust_primitives.sequence.seq_from_array a
ok s
/-- Trait implementation: [alloc::vec::{impl core::convert::From<[T; N]> for alloc::vec::Vec<T>}]
Source: 'src/lib.rs', lines 1013:4-1017:5 -/
@[reducible]
def vec.Vec.Insts.CoreConvertFromArray (T : Type) (N : Std.Usize) :
core.convert.From (vec.Vec T) (Array T N) := {
«from» := vec.Vec.Insts.CoreConvertFromArray.from
}
end CoreModels.alloc