Documentation
Init
.
Data
.
Slice
.
Array
.
Lemmas
Search
return to top
source
Imports
Init.Data.Array.Subarray
Init.Data.Iterators.Lemmas
Init.Data.Slice.Lemmas
Init.Data.Slice.Operations
Init.Data.Range.Polymorphic.Iterators
Init.Data.Range.Polymorphic.Lemmas
Init.Data.Slice.Array.Basic
Init.Data.Slice.Array.Iterator
Init.Data.Slice.Array.Iterator
Imported by
Std
.
Slice
.
Array
.
instLawfulSliceSizeSubarrayData
source
instance
Std
.
Slice
.
Array
.
instLawfulSliceSizeSubarrayData
{
α
:
Type
u_1}
:
LawfulSliceSize
(
Internal.SubarrayData
α
)