ForIn.toList of the effect-free containers

Each bridge lemma computes ForIn.toList for one container, in the spelling that carries the membership lemmas the verification conditions need, and each instance records that the container's loop is effect-free.

@[simp]

theorem Std.Internal.ForIn.toList_list {γ : Type u₁} (xs : List γ) : ForIn.toList xs = xs

instance Std.Internal.instLawfulMemForInIdList {α : Type u₁} : LawfulMemForInId (List α) α

instance Std.Internal.instPureForIn'List {m : Type u → Type v} [Monad m] {α : Type u₁} : PureForIn' m (List α) α

instance Std.Internal.instPureForInList {m : Type u → Type v} [Monad m] {α : Type u₁} : PureForIn m (List α) α

@[simp]

theorem Std.Internal.ForIn.toList_array {γ : Type u₁} (xs : Array γ) : ForIn.toList xs = xs.toList

instance Std.Internal.instLawfulMemForInIdArray {α : Type u₁} : LawfulMemForInId (Array α) α

instance Std.Internal.instPureForIn'Array {m : Type u → Type v} [Monad m] {α : Type u₁} : PureForIn' m (Array α) α

instance Std.Internal.instPureForInArray {m : Type u → Type v} [Monad m] {α : Type u₁} : PureForIn m (Array α) α

@[simp]

theorem Std.Internal.ForIn.toList_range (r : Legacy.Range) : ForIn.toList r = List.range' r.start r.size r.step

instance Std.Internal.instLawfulMemForInIdRangeNat : LawfulMemForInId Legacy.Range Nat

instance Std.Internal.instPureForIn'RangeNat {m : Type u → Type v} [Monad m] : PureForIn' m Legacy.Range Nat

instance Std.Internal.instPureForInRangeNat {m : Type u → Type v} [Monad m] : PureForIn m Legacy.Range Nat

@[simp]

theorem Std.Internal.ForIn.toList_iter {α γ : Type w} [Iterator α Id γ] [Iterators.Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] (it : Iter γ) : ForIn.toList it = it.toList

ForIn.toList on an iterator is the iterator's own toList, so every container whose ForIn loop iterates its Std.ToIterator reaches the iterator lemmas through this one step.

instance Std.Internal.instPureForInIterOfLawfulMonadOfFiniteOfLawfulIteratorLoopId {α γ : Type w} {m : Type w → Type v} [Monad m] [LawfulMonad m] [Iterator α Id γ] [Iterators.Finite α Id] [IteratorLoop α Id m] [LawfulIteratorLoop α Id m] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] : PureForIn m (Iter γ) γ

@[simp]

theorem Std.Internal.ForIn.toList_iterM_id {α γ : Type w} [Iterator α Id γ] [Iterators.Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] (it : IterM Id γ) : ForIn.toList it = it.toList.run

ForIn.toList on a pure monadic iterator is the iterator's own toList.

instance Std.Internal.instPureForInIterMIdOfLawfulMonadOfFiniteOfLawfulIteratorLoop {α γ : Type w} {m : Type w → Type v} [Monad m] [LawfulMonad m] [Iterator α Id γ] [Iterators.Finite α Id] [IteratorLoop α Id m] [LawfulIteratorLoop α Id m] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] : PureForIn m (IterM Id γ) γ

theorem Std.Internal.ForIn.toList_rcc {α : Type u} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] (r : Rcc α) : ForIn.toList r = r.toList

instance Std.Internal.instLawfulMemForInIdRcc {α : Type u} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] : LawfulMemForInId (Rcc α) α

instance Std.Internal.instPureForIn'RccOfLawfulMonad {α : Type u} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] {m : Type u → Type v} [Monad m] [LawfulMonad m] : PureForIn' m (Rcc α) α

instance Std.Internal.instPureForInRccOfLawfulMonad {α : Type u} [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] {m : Type u → Type v} [Monad m] [LawfulMonad m] : PureForIn m (Rcc α) α

theorem Std.Internal.ForIn.toList_rco {α : Type u} [LE α] [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.LawfulUpwardEnumerableLT α] (r : Rco α) : ForIn.toList r = r.toList

instance Std.Internal.instLawfulMemForInIdRco {α : Type u} [LE α] [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.LawfulUpwardEnumerableLT α] : LawfulMemForInId (Rco α) α

instance Std.Internal.instPureForIn'RcoOfLawfulMonad {α : Type u} [LE α] [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.LawfulUpwardEnumerableLT α] {m : Type u → Type v} [Monad m] [LawfulMonad m] : PureForIn' m (Rco α) α

instance Std.Internal.instPureForInRcoOfLawfulMonad {α : Type u} [LE α] [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.LawfulUpwardEnumerableLT α] {m : Type u → Type v} [Monad m] [LawfulMonad m] : PureForIn m (Rco α) α

theorem Std.Internal.ForIn.toList_rci {α : Type u} [LE α] [PRange.UpwardEnumerable α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] (r : Rci α) : ForIn.toList r = r.toList

instance Std.Internal.instLawfulMemForInIdRci {α : Type u} [LE α] [PRange.UpwardEnumerable α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] : LawfulMemForInId (Rci α) α

instance Std.Internal.instPureForIn'RciOfLawfulMonad {α : Type u} [LE α] [PRange.UpwardEnumerable α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] {m : Type u → Type v} [Monad m] [LawfulMonad m] : PureForIn' m (Rci α) α

instance Std.Internal.instPureForInRciOfLawfulMonad {α : Type u} [LE α] [PRange.UpwardEnumerable α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] {m : Type u → Type v} [Monad m] [LawfulMonad m] : PureForIn m (Rci α) α

theorem Std.Internal.ForIn.toList_roc {α : Type u} [LE α] [DecidableLE α] [LT α] [PRange.UpwardEnumerable α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.LawfulUpwardEnumerableLT α] (r : Roc α) : ForIn.toList r = r.toList

instance Std.Internal.instLawfulMemForInIdRoc {α : Type u} [LE α] [DecidableLE α] [LT α] [PRange.UpwardEnumerable α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.LawfulUpwardEnumerableLT α] : LawfulMemForInId (Roc α) α

instance Std.Internal.instPureForIn'RocOfLawfulMonad {α : Type u} [LE α] [DecidableLE α] [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.LawfulUpwardEnumerableLT α] {m : Type u → Type v} [Monad m] [LawfulMonad m] : PureForIn' m (Roc α) α

instance Std.Internal.instPureForInRocOfLawfulMonad {α : Type u} [LE α] [DecidableLE α] [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLE α] [PRange.LawfulUpwardEnumerableLT α] {m : Type u → Type v} [Monad m] [LawfulMonad m] : PureForIn m (Roc α) α

theorem Std.Internal.ForIn.toList_roo {α : Type u} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] (r : Roo α) : ForIn.toList r = r.toList

instance Std.Internal.instLawfulMemForInIdRoo {α : Type u} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] : LawfulMemForInId (Roo α) α

instance Std.Internal.instPureForIn'RooOfLawfulMonad {α : Type u} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] {m : Type u → Type v} [Monad m] [LawfulMonad m] : PureForIn' m (Roo α) α

instance Std.Internal.instPureForInRooOfLawfulMonad {α : Type u} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] {m : Type u → Type v} [Monad m] [LawfulMonad m] : PureForIn m (Roo α) α

theorem Std.Internal.ForIn.toList_roi {α : Type u} [LT α] [PRange.UpwardEnumerable α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] (r : Roi α) : ForIn.toList r = r.toList

instance Std.Internal.instLawfulMemForInIdRoi {α : Type u} [LT α] [PRange.UpwardEnumerable α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] : LawfulMemForInId (Roi α) α

instance Std.Internal.instPureForIn'RoiOfLawfulMonad {α : Type u} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] {m : Type u → Type v} [Monad m] [LawfulMonad m] : PureForIn' m (Roi α) α

instance Std.Internal.instPureForInRoiOfLawfulMonad {α : Type u} [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLT α] {m : Type u → Type v} [Monad m] [LawfulMonad m] : PureForIn m (Roi α) α

theorem Std.Internal.ForIn.toList_ric {α : Type u} [PRange.Least? α] [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLeast? α] [PRange.LawfulUpwardEnumerableLE α] (r : Ric α) : ForIn.toList r = r.toList

instance Std.Internal.instLawfulMemForInIdRic {α : Type u} [PRange.Least? α] [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLeast? α] [PRange.LawfulUpwardEnumerableLE α] : LawfulMemForInId (Ric α) α

instance Std.Internal.instPureForIn'RicOfLawfulMonad {α : Type u} [PRange.Least? α] [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLeast? α] [PRange.LawfulUpwardEnumerableLE α] {m : Type u → Type v} [Monad m] [LawfulMonad m] : PureForIn' m (Ric α) α

instance Std.Internal.instPureForInRicOfLawfulMonad {α : Type u} [PRange.Least? α] [LE α] [DecidableLE α] [PRange.UpwardEnumerable α] [Rxc.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLeast? α] [PRange.LawfulUpwardEnumerableLE α] {m : Type u → Type v} [Monad m] [LawfulMonad m] : PureForIn m (Ric α) α

theorem Std.Internal.ForIn.toList_rio {α : Type u} [PRange.Least? α] [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLeast? α] [PRange.LawfulUpwardEnumerableLT α] (r : Rio α) : ForIn.toList r = r.toList

instance Std.Internal.instLawfulMemForInIdRio {α : Type u} [PRange.Least? α] [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLeast? α] [PRange.LawfulUpwardEnumerableLT α] : LawfulMemForInId (Rio α) α

instance Std.Internal.instPureForIn'RioOfLawfulMonad {α : Type u} [PRange.Least? α] [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLeast? α] [PRange.LawfulUpwardEnumerableLT α] {m : Type u → Type v} [Monad m] [LawfulMonad m] : PureForIn' m (Rio α) α

instance Std.Internal.instPureForInRioOfLawfulMonad {α : Type u} [PRange.Least? α] [LT α] [DecidableLT α] [PRange.UpwardEnumerable α] [Rxo.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLeast? α] [PRange.LawfulUpwardEnumerableLT α] {m : Type u → Type v} [Monad m] [LawfulMonad m] : PureForIn m (Rio α) α

theorem Std.Internal.ForIn.toList_rii {α : Type u} [PRange.Least? α] [PRange.UpwardEnumerable α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLeast? α] (r : Rii α) : ForIn.toList r = r.toList

instance Std.Internal.instLawfulMemForInIdRii {α : Type u} [PRange.Least? α] [PRange.UpwardEnumerable α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLeast? α] : LawfulMemForInId (Rii α) α

instance Std.Internal.instPureForIn'RiiOfLawfulMonad {α : Type u} [LT α] [PRange.Least? α] [PRange.UpwardEnumerable α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLeast? α] [PRange.LawfulUpwardEnumerableLT α] {m : Type u → Type v} [Monad m] [LawfulMonad m] : PureForIn' m (Rii α) α

instance Std.Internal.instPureForInRiiOfLawfulMonad {α : Type u} [LT α] [PRange.Least? α] [PRange.UpwardEnumerable α] [Rxi.IsAlwaysFinite α] [PRange.LawfulUpwardEnumerable α] [PRange.LawfulUpwardEnumerableLeast? α] [PRange.LawfulUpwardEnumerableLT α] {m : Type u → Type v} [Monad m] [LawfulMonad m] : PureForIn m (Rii α) α

@[simp]

theorem Std.Internal.ForIn.toList_slice {γ : Type u} {α γ' : Type w} [ToIterator (Slice γ) Id α γ'] [Iterator α Id γ'] [Iterators.Finite α Id] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] (s : Slice γ) : ForIn.toList s = s.toList

ForIn.toList on a slice is the slice's own toList.

instance Std.Internal.instPureForInSliceOfLawfulMonadOfFiniteOfLawfulIteratorLoopId {γ : Type u} {α γ' : Type w} {m : Type w → Type v} [Monad m] [LawfulMonad m] [ToIterator (Slice γ) Id α γ'] [Iterator α Id γ'] [Iterators.Finite α Id] [IteratorLoop α Id m] [LawfulIteratorLoop α Id m] [IteratorLoop α Id Id] [LawfulIteratorLoop α Id Id] : PureForIn m (Slice γ) γ'