Documentation

Init.Data.Slice.List.Lemmas

Imports

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.List.Basic
Init.Data.Slice.List.Iterator
Init.Data.Slice.List.Iterator

Imported by

Std.Slice.List.instLawfulSliceSizeListSliceData

instance Std.Slice.List.instLawfulSliceSizeListSliceData {α : Type u_1} :

LawfulSliceSize (Internal.ListSliceData α)