diff options
Diffstat (limited to 'backends/lean/Base/Primitives/ArraySlice.lean')
-rw-r--r-- | backends/lean/Base/Primitives/ArraySlice.lean | 61 |
1 files changed, 59 insertions, 2 deletions
diff --git a/backends/lean/Base/Primitives/ArraySlice.lean b/backends/lean/Base/Primitives/ArraySlice.lean index 47807a0d..615e0783 100644 --- a/backends/lean/Base/Primitives/ArraySlice.lean +++ b/backends/lean/Base/Primitives/ArraySlice.lean @@ -13,7 +13,7 @@ import Base.Progress.Base namespace Primitives -open Result Error +open Result Error core.ops.range def Array (α : Type u) (n : Usize) := { l : List α // l.length = n.val } @@ -406,7 +406,7 @@ structure core.slice.index.private_slice_index.Sealed (Self : Type) where /- Trait declaration: [core::slice::index::SliceIndex] -/ structure core.slice.index.SliceIndex (Self T0 : Type) where - sealedInst :core.slice.index.private_slice_index.Sealed Self + sealedInst : core.slice.index.private_slice_index.Sealed Self Output : Type get : Self → T0 → Result (Option Output) get_mut : Self → T0 → Result (Option Output) @@ -557,4 +557,61 @@ def core.array.Array.coreopsindexIndexMutInst (T0 I : Type) (N : Usize) index_mut_back := core.array.Array.index_mut_back T0 I N inst } +/- [core::slice::index::usize::get]: forward function -/ +def core.slice.index.Usize.get + (T : Type) : Usize → Slice T → Result (Option T) := + sorry -- TODO + +/- [core::slice::index::usize::get_mut]: forward function -/ +def core.slice.index.Usize.get_mut + (T : Type) : Usize → Slice T → Result (Option T) := + sorry -- TODO + +/- [core::slice::index::usize::get_mut]: backward function 0 -/ +def core.slice.index.Usize.get_mut_back + (T : Type) : Usize → Slice T → Option T → Result (Slice T) := + sorry -- TODO + +/- [core::slice::index::usize::get_unchecked]: forward function -/ +def core.slice.index.Usize.get_unchecked + (T : Type) : Usize → ConstRawPtr (Slice T) → Result (ConstRawPtr T) := + sorry -- TODO + +/- [core::slice::index::usize::get_unchecked_mut]: forward function -/ +def core.slice.index.Usize.get_unchecked_mut + (T : Type) : Usize → MutRawPtr (Slice T) → Result (MutRawPtr T) := + sorry -- TODO + +/- [core::slice::index::usize::index]: forward function -/ +def core.slice.index.Usize.index (T : Type) : Usize → Slice T → Result T := + sorry -- TODO + +/- [core::slice::index::usize::index_mut]: forward function -/ +def core.slice.index.Usize.index_mut (T : Type) : Usize → Slice T → Result T := + sorry -- TODO + +/- [core::slice::index::usize::index_mut]: backward function 0 -/ +def core.slice.index.Usize.index_mut_back + (T : Type) : Usize → Slice T → T → Result (Slice T) := + sorry -- TODO + +/- Trait implementation: [core::slice::index::private_slice_index::usize] -/ +def core.slice.index.private_slice_index.usize.coresliceindexprivate_slice_indexSealedInst + : core.slice.index.private_slice_index.Sealed Usize := {} + +/- Trait implementation: [core::slice::index::usize] -/ +def core.slice.index.usize.coresliceindexSliceIndexInst (T : Type) : + core.slice.index.SliceIndex Usize (Slice T) := { + sealedInst := core.slice.index.private_slice_index.usize.coresliceindexprivate_slice_indexSealedInst + Output := T + get := core.slice.index.Usize.get T + get_mut := core.slice.index.Usize.get_mut T + get_mut_back := core.slice.index.Usize.get_mut_back T + get_unchecked := core.slice.index.Usize.get_unchecked T + get_unchecked_mut := core.slice.index.Usize.get_unchecked_mut T + index := core.slice.index.Usize.index T + index_mut := core.slice.index.Usize.index_mut T + index_mut_back := core.slice.index.Usize.index_mut_back T +} + end Primitives |