20.18. 范围🔗

范围表示某种类型的连续元素序列，从下界到上界。边界可以是开的，在这种情况下，边界值不属于该范围，也可以是闭的，在这种情况下，边界值属于该范围。任一边界都可以被省略，在这种情况下，范围在相应的方向上无限延伸。

范围具有专用语法，包括一个起点、... 和一个终点。起点可以是 *，表示向下无限延伸的范围，也可以是一个项，表示具有特定起始值的范围。默认情况下，范围是左闭的：它们包含其起点。尾部的 < 表示该范围是左开的并且不包含其起点。终点可以是 *，在这种情况下范围向上无限延伸，也可以是一个项，表示具有特定结束值的范围。默认情况下，范围是右开的：它们不包含其终点。终点可以前缀 < 以表示它是右开的；这是默认行为，不会改变含义，但可能更容易阅读。它也可以前缀 = 以表示该范围是右闭的并且包含其终点。

自然数范围

包含数字 3 到 6 的范围可以用多种方式编写：

[3, 4, 5, 6]#eval (3...7).toList

[3, 4, 5, 6]

[3, 4, 5, 6]#eval (3...=6).toList

[3, 4, 5, 6]

[3, 4, 5, 6]#eval (2<...=6).toList

[3, 4, 5, 6]

在线查看 ↪

有限范围和无限范围

该范围不能转换为列表，因为它是无限的：

#eval failed to synthesize instance of type class
  Std.Rxi.IsAlwaysFinite Nat

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.(3...*).toList

左闭右无界范围的有限性通过 Std.Rxi.IsAlwaysFinite 实例的存在来指示，而 Nat 不存在该实例。 Std.Rco 是这些范围的类型，而名称 Std.Rxi.IsAlwaysFinite 表明它决定了所有右无界范围的有限性。

failed to synthesize instance of type class
  Std.Rxi.IsAlwaysFinite Nat

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.

尝试枚举负整数会导致类似的错误，这次是因为无法确定最小元素：

#eval failed to synthesize instance of type class
  Std.PRange.Least? Int

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.(*...(0 : Int)).toList

failed to synthesize instance of type class
  Std.PRange.Least? Int

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.

有限类型中的无界范围表示该范围延伸到该类型的最大元素。因为 UInt8 有 256 个元素，所以此范围包含 253 个元素：

253#eval ((3 : UInt8)...*).toArray.size

在线查看 ↪

语法范围语法

该范围是左闭右开的，并指示 Std.Rco：

term ::= ...
    | term...term

该范围是左闭右开的，并指示 Std.Rco：

term ::= ...
    | term...<term

该范围是左闭右闭的，并指示 Std.Rcc：

term ::= ...
    | term...=term

该范围是左闭右无限的，并指示 Std.Rci：

term ::= ...
    | term...*

该范围是左开右开的，并指示 Std.Roo：

term ::= ...
    | term<...term

该范围是左开右开的，并指示 Std.Roo：

term ::= ...
    | term<...<term

该范围是左开右闭的，并指示 Std.Roc：

term ::= ...
    | term<...=term

该范围是左开右无限的，并指示 Std.Roi：

term ::= ...
    | term<...*

该范围是左无限右开的，并指示 Std.Rio：

term ::= ...
    | *...term

此范围左侧无界、右侧开放，表示 Std.Ric：

term ::= ...
    | *...<term

该范围是左无限右闭的，并指示 Std.Ric：

term ::= ...
    | *...=term

该范围两端都是无限的，并指示 Std.Rii：

term ::= ...
    | *...*

20.18.1. 范围类型🔗

结构体

Std.Rco.{u} (α : Type u) : Type u
Std.Rco.{u} (α : Type u) : Type u

α 中具有闭下界和开上界的区间。

a...b 或 a...<b 表示所有大于等于 a : α 且小于 b : α 的值。这是 Rco.mk a b 的记法。

构造子

Std.Rco.mk.{u}

字段

lower : α

范围的下限。lower 包含在范围内。

upper : α

范围的上限。upper 不包含在范围内。

定义

Std.Rco.iter.{u_1} {α : Type u_1} (r : Std.Rco α) : Std.Iter α
Std.Rco.iter.{u_1} {α : Type u_1}
  (r : Std.Rco α) : Std.Iter α

返回给定范围的迭代器。该迭代器将按递增顺序生成范围内的元素。

定义

Std.Rco.toArray.{u} {α : Type u} [LT α] [DecidableLT α]
  [Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerable α]
  [Std.Rxo.IsAlwaysFinite α] (r : Std.Rco α) : Array α
Std.Rco.toArray.{u} {α : Type u} [LT α]
  [DecidableLT α]
  [Std.PRange.UpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerable α]
  [Std.Rxo.IsAlwaysFinite α]
  (r : Std.Rco α) : Array α

以升序将给定的左闭右开区间的元素作为数组返回。

定义

Std.Rco.toList.{u} {α : Type u} [LT α] [DecidableLT α]
  [Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerable α]
  [Std.Rxo.IsAlwaysFinite α] (r : Std.Rco α) : List α
Std.Rco.toList.{u} {α : Type u} [LT α]
  [DecidableLT α]
  [Std.PRange.UpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerable α]
  [Std.Rxo.IsAlwaysFinite α]
  (r : Std.Rco α) : List α

将给定的左闭右开范围的元素作为列表按升序返回。

定义

Std.Rco.size.{u} {α : Type u} [Std.Rxo.HasSize α] (r : Std.Rco α) : Nat
Std.Rco.size.{u} {α : Type u}
  [Std.Rxo.HasSize α] (r : Std.Rco α) :
  Nat

返回给定左闭右开区间中包含的元素数量。

定义

Std.Rco.isEmpty.{u} {α : Type u} [LT α] [DecidableLT α]
  [Std.PRange.UpwardEnumerable α] (r : Std.Rco α) : Bool
Std.Rco.isEmpty.{u} {α : Type u} [LT α]
  [DecidableLT α]
  [Std.PRange.UpwardEnumerable α]
  (r : Std.Rco α) : Bool

检查范围内是否包含任何值。

该函数在给定 LawfulUpwardEnumerable 和 LawfulUpwardEnumerableLT 实例时返回一个有意义的值。

结构体

Std.Rcc.{u} (α : Type u) : Type u
Std.Rcc.{u} (α : Type u) : Type u

具有闭合上下界的α的一系列元素。

a...=b 是所有大于或等于 a : α 并且小于或等于 b : α 的值的范围。这是 Rcc.mk a b 的表示法。

构造子

Std.Rcc.mk.{u}

字段

lower : α

范围的下限。lower 包含在范围内。

upper : α

范围的上限。upper 包含在范围内。

定义

Std.Rcc.iter.{u_1} {α : Type u_1} (r : Std.Rcc α) : Std.Iter α
Std.Rcc.iter.{u_1} {α : Type u_1}
  (r : Std.Rcc α) : Std.Iter α

返回给定范围的迭代器。该迭代器将按递增顺序生成范围内的元素。

定义

Std.Rcc.toArray.{u} {α : Type u} [LE α] [DecidableLE α]
  [Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerable α]
  [Std.Rxc.IsAlwaysFinite α] (r : Std.Rcc α) : Array α
Std.Rcc.toArray.{u} {α : Type u} [LE α]
  [DecidableLE α]
  [Std.PRange.UpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerable α]
  [Std.Rxc.IsAlwaysFinite α]
  (r : Std.Rcc α) : Array α

以升序将给定闭区间的元素作为数组返回。

定义

Std.Rcc.toList.{u} {α : Type u} [LE α] [DecidableLE α]
  [Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerable α]
  [Std.Rxc.IsAlwaysFinite α] (r : Std.Rcc α) : List α
Std.Rcc.toList.{u} {α : Type u} [LE α]
  [DecidableLE α]
  [Std.PRange.UpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerable α]
  [Std.Rxc.IsAlwaysFinite α]
  (r : Std.Rcc α) : List α

以升序将给定闭区间的元素作为列表返回。

定义

Std.Rcc.size.{u} {α : Type u} [Std.Rxc.HasSize α] (r : Std.Rcc α) : Nat
Std.Rcc.size.{u} {α : Type u}
  [Std.Rxc.HasSize α] (r : Std.Rcc α) :
  Nat

返回给定闭区间中包含的元素数量。

定义

Std.Rcc.isEmpty.{u} {α : Type u} [LE α] [DecidableLE α]
  [Std.PRange.UpwardEnumerable α] (r : Std.Rcc α) : Bool
Std.Rcc.isEmpty.{u} {α : Type u} [LE α]
  [DecidableLE α]
  [Std.PRange.UpwardEnumerable α]
  (r : Std.Rcc α) : Bool

检查范围内是否包含任何值。

该函数在给定 LawfulUpwardEnumerable 和 LawfulUpwardEnumerableLE 实例时返回一个有意义的值。

结构体

Std.Rci.{u} (α : Type u) : Type u
Std.Rci.{u} (α : Type u) : Type u

α 中具有闭下界、向上无界的区间。

a...* 表示所有大于等于 a : α 的值。这是 Rci.mk a 的记法。

构造子

Std.Rci.mk.{u}

字段

lower : α

范围的下限。lower 包含在范围内。

定义

Std.Rci.iter.{u_1} {α : Type u_1} (r : Std.Rci α) : Std.Iter α
Std.Rci.iter.{u_1} {α : Type u_1}
  (r : Std.Rci α) : Std.Iter α

返回给定范围的迭代器。该迭代器将按递增顺序生成范围内的元素。

定义

Std.Rci.toArray.{u} {α : Type u} [Std.PRange.UpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerable α] [Std.Rxi.IsAlwaysFinite α]
  (r : Std.Rci α) : Array α
Std.Rci.toArray.{u} {α : Type u}
  [Std.PRange.UpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerable α]
  [Std.Rxi.IsAlwaysFinite α]
  (r : Std.Rci α) : Array α

以升序返回给定左闭右无界范围的元素数组。

定义

Std.Rci.toList.{u} {α : Type u} [Std.PRange.UpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerable α] [Std.Rxi.IsAlwaysFinite α]
  (r : Std.Rci α) : List α
Std.Rci.toList.{u} {α : Type u}
  [Std.PRange.UpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerable α]
  [Std.Rxi.IsAlwaysFinite α]
  (r : Std.Rci α) : List α

将给定的左闭右开区间的元素作为列表按升序返回。

定义

Std.Rci.size.{u} {α : Type u} [Std.Rxi.HasSize α] (r : Std.Rci α) : Nat
Std.Rci.size.{u} {α : Type u}
  [Std.Rxi.HasSize α] (r : Std.Rci α) :
  Nat

返回给定左闭右开区间中包含的元素数量。

定义

Std.Rci.isEmpty.{u} {α : Type u} [Std.PRange.UpwardEnumerable α] :
  Std.Rci α → Bool
Std.Rci.isEmpty.{u} {α : Type u}
  [Std.PRange.UpwardEnumerable α] :
  Std.Rci α → Bool

检查范围是否包含任何值。此函数存在是为了完整性，并且总是返回 false：闭合的下界包含在范围内，因此左闭右无界的范围永远不为空。

结构体

Std.Roo.{u} (α : Type u) : Type u
Std.Roo.{u} (α : Type u) : Type u

α 中下界和上界均为开的区间。

a<...b 或 a<...<b 表示所有大于 a : α 且小于 b : α 的值。这是 Roo.mk a b 的记法。

构造子

Std.Roo.mk.{u}

字段

lower : α

范围的下界。lower不包含在范围内。

upper : α

范围的上限。upper 不包含在范围内。

定义

Std.Roo.iter.{u_1} {α : Type u_1} [Std.PRange.UpwardEnumerable α]
  (r : Std.Roo α) : Std.Iter α
Std.Roo.iter.{u_1} {α : Type u_1}
  [Std.PRange.UpwardEnumerable α]
  (r : Std.Roo α) : Std.Iter α

返回给定范围的迭代器。该迭代器将按递增顺序生成范围内的元素。

定义

Std.Roo.toArray.{u} {α : Type u} [LT α] [DecidableLT α]
  [Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerable α]
  [Std.Rxo.IsAlwaysFinite α] (r : Std.Roo α) : Array α
Std.Roo.toArray.{u} {α : Type u} [LT α]
  [DecidableLT α]
  [Std.PRange.UpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerable α]
  [Std.Rxo.IsAlwaysFinite α]
  (r : Std.Roo α) : Array α

以升序将给定开区间的元素作为数组返回。

定义

Std.Roo.toList.{u} {α : Type u} [LT α] [DecidableLT α]
  [Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerable α]
  [Std.Rxo.IsAlwaysFinite α] (r : Std.Roo α) : List α
Std.Roo.toList.{u} {α : Type u} [LT α]
  [DecidableLT α]
  [Std.PRange.UpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerable α]
  [Std.Rxo.IsAlwaysFinite α]
  (r : Std.Roo α) : List α

以升序将给定开区间的元素作为列表返回。

定义

Std.Roo.size.{u} {α : Type u} [Std.Rxo.HasSize α]
  [Std.PRange.UpwardEnumerable α] (r : Std.Roo α) : Nat
Std.Roo.size.{u} {α : Type u}
  [Std.Rxo.HasSize α]
  [Std.PRange.UpwardEnumerable α]
  (r : Std.Roo α) : Nat

返回给定开区间中包含的元素数量。

定义

Std.Roo.isEmpty.{u} {α : Type u} [LT α] [DecidableLT α]
  [Std.PRange.UpwardEnumerable α] (r : Std.Roo α) : Bool
Std.Roo.isEmpty.{u} {α : Type u} [LT α]
  [DecidableLT α]
  [Std.PRange.UpwardEnumerable α]
  (r : Std.Roo α) : Bool

检查范围内是否包含任何值。

该函数在给定 LawfulUpwardEnumerable 和 LawfulUpwardEnumerableLT 实例时返回一个有意义的值。

结构体

Std.Roc.{u} (α : Type u) : Type u
Std.Roc.{u} (α : Type u) : Type u

α 的一系列元素，具有开下界和闭上界。

a<...=b 是所有大于 a : α 且小于或等于 b : α 的值的范围。这是 Roc.mk a b 的表示法。

构造子

Std.Roc.mk.{u}

字段

lower : α

范围的下界。lower不包含在范围内。

upper : α

范围的上限。upper 包含在范围内。

定义

Std.Roc.iter.{u_1} {α : Type u_1} [Std.PRange.UpwardEnumerable α]
  (r : Std.Roc α) : Std.Iter α
Std.Roc.iter.{u_1} {α : Type u_1}
  [Std.PRange.UpwardEnumerable α]
  (r : Std.Roc α) : Std.Iter α

返回给定范围的迭代器。该迭代器将按递增顺序生成范围内的元素。

定义

Std.Roc.toArray.{u} {α : Type u} [LE α] [DecidableLE α]
  [Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerable α]
  [Std.Rxc.IsAlwaysFinite α] (r : Std.Roc α) : Array α
Std.Roc.toArray.{u} {α : Type u} [LE α]
  [DecidableLE α]
  [Std.PRange.UpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerable α]
  [Std.Rxc.IsAlwaysFinite α]
  (r : Std.Roc α) : Array α

以升序将给定的左开右闭区间的元素作为数组返回。

定义

Std.Roc.toList.{u} {α : Type u} [LE α] [DecidableLE α]
  [Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerable α]
  [Std.Rxc.IsAlwaysFinite α] (r : Std.Roc α) : List α
Std.Roc.toList.{u} {α : Type u} [LE α]
  [DecidableLE α]
  [Std.PRange.UpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerable α]
  [Std.Rxc.IsAlwaysFinite α]
  (r : Std.Roc α) : List α

以升序将给定的左开右闭区间的元素作为列表返回。

定义

Std.Roc.size.{u} {α : Type u} [Std.Rxc.HasSize α]
  [Std.PRange.UpwardEnumerable α] (r : Std.Roc α) : Nat
Std.Roc.size.{u} {α : Type u}
  [Std.Rxc.HasSize α]
  [Std.PRange.UpwardEnumerable α]
  (r : Std.Roc α) : Nat

返回给定左开右闭区间中包含的元素数量。

定义

Std.Roc.isEmpty.{u} {α : Type u} [LT α] [DecidableLT α]
  [Std.PRange.UpwardEnumerable α] (r : Std.Roc α) : Bool
Std.Roc.isEmpty.{u} {α : Type u} [LT α]
  [DecidableLT α]
  [Std.PRange.UpwardEnumerable α]
  (r : Std.Roc α) : Bool

检查范围内是否包含任何值。

该函数在给定 LawfulUpwardEnumerable 和 LawfulUpwardEnumerableLT 实例时返回一个有意义的值。

结构体

Std.Roi.{u} (α : Type u) : Type u
Std.Roi.{u} (α : Type u) : Type u

α 中具有开下界、向上无界的区间。

a<...* 表示所有大于 a : α 的值。这是 Roi.mk a 的记法。

构造子

Std.Roi.mk.{u}

字段

lower : α

范围的下界。lower不包含在范围内。

定义

Std.Roi.iter.{u_1} {α : Type u_1} [Std.PRange.UpwardEnumerable α]
  (r : Std.Roi α) : Std.Iter α
Std.Roi.iter.{u_1} {α : Type u_1}
  [Std.PRange.UpwardEnumerable α]
  (r : Std.Roi α) : Std.Iter α

返回给定范围的迭代器。该迭代器将按递增顺序生成范围内的元素。

定义

Std.Roi.toArray.{u} {α : Type u} [Std.PRange.UpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerable α] [Std.Rxi.IsAlwaysFinite α]
  (r : Std.Roi α) : Array α
Std.Roi.toArray.{u} {α : Type u}
  [Std.PRange.UpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerable α]
  [Std.Rxi.IsAlwaysFinite α]
  (r : Std.Roi α) : Array α

以升序将给定的左开右无界范围的元素作为数组返回。

定义

Std.Roi.toList.{u} {α : Type u} [Std.PRange.UpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerable α] [Std.Rxi.IsAlwaysFinite α]
  (r : Std.Roi α) : List α
Std.Roi.toList.{u} {α : Type u}
  [Std.PRange.UpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerable α]
  [Std.Rxi.IsAlwaysFinite α]
  (r : Std.Roi α) : List α

将给定的左开右无界区间的元素作为列表按升序返回。

定义

Std.Roi.size.{u} {α : Type u} [Std.Rxi.HasSize α]
  [Std.PRange.UpwardEnumerable α] (r : Std.Roi α) : Nat
Std.Roi.size.{u} {α : Type u}
  [Std.Rxi.HasSize α]
  [Std.PRange.UpwardEnumerable α]
  (r : Std.Roi α) : Nat

返回给定左开右无限区间中包含的元素数量。

定义

Std.Roi.isEmpty.{u} {α : Type u} [Std.PRange.UpwardEnumerable α]
  (r : Std.Roi α) : Bool
Std.Roi.isEmpty.{u} {α : Type u}
  [Std.PRange.UpwardEnumerable α]
  (r : Std.Roi α) : Bool

检查范围内是否包含任何值。

此函数在给定 LawfulUpwardEnumerable 实例时返回一个有意义的值。

结构体

Std.Rio.{u} (α : Type u) : Type u
Std.Rio.{u} (α : Type u) : Type u

α 中具有开上界、向下无界的区间。

*...b 或 *...<b 表示所有小于 b : α 的值。这是 Rio.mk b 的记法。

构造子

Std.Rio.mk.{u}

字段

upper : α

范围的上限。upper 不包含在范围内。

定义

Std.Rio.iter.{u_1} {α : Type u_1} [Std.PRange.Least? α]
  (r : Std.Rio α) : Std.Iter α
Std.Rio.iter.{u_1} {α : Type u_1}
  [Std.PRange.Least? α] (r : Std.Rio α) :
  Std.Iter α

返回给定范围的迭代器。该迭代器将按递增顺序生成范围内的元素。

定义

Std.Rio.toArray.{u} {α : Type u} [Std.PRange.Least? α] [LT α]
  [DecidableLT α] [Std.PRange.UpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerable α] [Std.Rxo.IsAlwaysFinite α]
  (r : Std.Rio α) : Array α
Std.Rio.toArray.{u} {α : Type u}
  [Std.PRange.Least? α] [LT α]
  [DecidableLT α]
  [Std.PRange.UpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerable α]
  [Std.Rxo.IsAlwaysFinite α]
  (r : Std.Rio α) : Array α

以升序将给定闭区间的元素作为数组返回。

定义

Std.Rio.toList.{u} {α : Type u} [Std.PRange.Least? α] [LT α]
  [DecidableLT α] [Std.PRange.UpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerable α] [Std.Rxo.IsAlwaysFinite α]
  (r : Std.Rio α) : List α
Std.Rio.toList.{u} {α : Type u}
  [Std.PRange.Least? α] [LT α]
  [DecidableLT α]
  [Std.PRange.UpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerable α]
  [Std.Rxo.IsAlwaysFinite α]
  (r : Std.Rio α) : List α

以升序将给定闭区间的元素作为列表返回。

定义

Std.Rio.size.{u} {α : Type u} [Std.Rxo.HasSize α] [Std.PRange.Least? α]
  (r : Std.Rio α) : Nat
Std.Rio.size.{u} {α : Type u}
  [Std.Rxo.HasSize α]
  [Std.PRange.Least? α] (r : Std.Rio α) :
  Nat

返回给定闭区间中包含的元素数量。

定义

Std.Rio.isEmpty.{u} {α : Type u} [LT α] [DecidableLT α]
  [Std.PRange.UpwardEnumerable α] [Std.PRange.Least? α]
  (r : Std.Rio α) : Bool
Std.Rio.isEmpty.{u} {α : Type u} [LT α]
  [DecidableLT α]
  [Std.PRange.UpwardEnumerable α]
  [Std.PRange.Least? α] (r : Std.Rio α) :
  Bool

检查范围内是否包含任何值。

该函数在给定 LawfulUpwardEnumerable、LawfulUpwardEnumerableLT 和 LawfulUpwardEnumerableLeast? 实例时返回一个有意义的值。

结构体

Std.Ric.{u} (α : Type u) : Type u
Std.Ric.{u} (α : Type u) : Type u

α 中具有闭上界、向下无界的区间。

*...=b 表示所有小于等于 b : α 的值。这是 Ric.mk b 的记法。

构造子

Std.Ric.mk.{u}

字段

upper : α

范围的上限。upper 包含在范围内。

定义

Std.Ric.iter.{u_1} {α : Type u_1} [Std.PRange.Least? α]
  (r : Std.Ric α) : Std.Iter α
Std.Ric.iter.{u_1} {α : Type u_1}
  [Std.PRange.Least? α] (r : Std.Ric α) :
  Std.Iter α

返回给定范围的迭代器。该迭代器将按递增顺序生成范围内的元素。

定义

Std.Ric.toArray.{u} {α : Type u} [Std.PRange.Least? α] [LE α]
  [DecidableLE α] [Std.PRange.UpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerable α] [Std.Rxc.IsAlwaysFinite α]
  (r : Std.Ric α) : Array α
Std.Ric.toArray.{u} {α : Type u}
  [Std.PRange.Least? α] [LE α]
  [DecidableLE α]
  [Std.PRange.UpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerable α]
  [Std.Rxc.IsAlwaysFinite α]
  (r : Std.Ric α) : Array α

以升序将给定闭区间的元素作为数组返回。

定义

Std.Ric.toList.{u} {α : Type u} [Std.PRange.Least? α] [LE α]
  [DecidableLE α] [Std.PRange.UpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerable α] [Std.Rxc.IsAlwaysFinite α]
  (r : Std.Ric α) : List α
Std.Ric.toList.{u} {α : Type u}
  [Std.PRange.Least? α] [LE α]
  [DecidableLE α]
  [Std.PRange.UpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerable α]
  [Std.Rxc.IsAlwaysFinite α]
  (r : Std.Ric α) : List α

以升序将给定闭区间的元素作为列表返回。

定义

Std.Ric.size.{u} {α : Type u} [Std.Rxc.HasSize α] [Std.PRange.Least? α]
  (r : Std.Ric α) : Nat
Std.Ric.size.{u} {α : Type u}
  [Std.Rxc.HasSize α]
  [Std.PRange.Least? α] (r : Std.Ric α) :
  Nat

返回给定闭区间中包含的元素数量。

定义

Std.Ric.isEmpty.{u} {α : Type u} [Std.PRange.UpwardEnumerable α] :
  Std.Ric α → Bool
Std.Ric.isEmpty.{u} {α : Type u}
  [Std.PRange.UpwardEnumerable α] :
  Std.Ric α → Bool

检查范围是否包含任何值。该函数存在是为了完整性，并且总是返回 false：闭合的上界包含在范围内，因此左无界右闭合的范围从不为空。

结构体

Std.Rii.{u} (α : Type u) : Type
Std.Rii.{u} (α : Type u) : Type

α 所有元素构成的全区间。它唯一的值是区间 *...*，这是 Rii.mk 的记法。

构造子

Std.Rii.mk.{u}

定义

Std.Rii.iter.{u_1} {α : Type u_1} [Std.PRange.Least? α] :
  Std.Rii α → Std.Iter α
Std.Rii.iter.{u_1} {α : Type u_1}
  [Std.PRange.Least? α] :
  Std.Rii α → Std.Iter α

返回给定范围的迭代器。该迭代器将按递增顺序生成范围内的元素。

定义

Std.Rii.toArray.{u_1} {α : Type u_1} [Std.PRange.UpwardEnumerable α]
  [Std.PRange.Least? α] (r : Std.Rii α)
  [Std.Iterator (Std.Rxi.Iterator α) Id α]
  [Std.Iterators.Finite (Std.Rxi.Iterator α) Id] : Array α
Std.Rii.toArray.{u_1} {α : Type u_1}
  [Std.PRange.UpwardEnumerable α]
  [Std.PRange.Least? α] (r : Std.Rii α)
  [Std.Iterator (Std.Rxi.Iterator α) Id α]
  [Std.Iterators.Finite
      (Std.Rxi.Iterator α) Id] :
  Array α

以升序将给定完整范围的元素作为数组返回。

定义

Std.Rii.toList.{u} {α : Type u} [Std.PRange.UpwardEnumerable α]
  [Std.PRange.Least? α] (r : Std.Rii α)
  [Std.Iterator (Std.Rxi.Iterator α) Id α]
  [Std.Iterators.Finite (Std.Rxi.Iterator α) Id] : List α
Std.Rii.toList.{u} {α : Type u}
  [Std.PRange.UpwardEnumerable α]
  [Std.PRange.Least? α] (r : Std.Rii α)
  [Std.Iterator (Std.Rxi.Iterator α) Id α]
  [Std.Iterators.Finite
      (Std.Rxi.Iterator α) Id] :
  List α

以升序将给定完整范围的元素作为列表返回。

定义

Std.Rii.size.{u} {α : Type u} :
  Std.Rii α → [Std.PRange.Least? α] → [Std.Rxi.HasSize α] → Nat
Std.Rii.size.{u} {α : Type u} :
  Std.Rii α →
    [Std.PRange.Least? α] →
      [Std.Rxi.HasSize α] → Nat

返回完整范围中包含的元素数量。

定义

Std.Rii.isEmpty.{u} {α : Type u} [Std.PRange.Least? α] :
  Std.Rii α → Bool
Std.Rii.isEmpty.{u} {α : Type u}
  [Std.PRange.Least? α] : Std.Rii α → Bool

检查范围内是否包含任何值。

该函数在给定 LawfulUpwardEnumerable 和 LawfulUpwardEnumerableLeast? 实例时返回一个有意义的值。

类型类

Std.PRange.UpwardEnumerable.{u} (α : Type u) : Type u
Std.PRange.UpwardEnumerable.{u}
  (α : Type u) : Type u

此类型类提供函数 succ? : α → Option α，用于计算 α 中元素的后继；不存在后继时返回 none。它还提供函数 succMany?，用于计算第 n 个后继。

succ? 应当无环：任何元素都不是自身的传递后继。如果 α 有序，则每个大于 a : α 的元素都应是 a 的传递后继。这些性质以及 succ? 与 succMany? 的兼容性由类型类 LawfulUpwardEnumerable、LawfulUpwardEnumerableLE 和 LawfulUpwardEnumerableLT 编码。

实例构造子

Std.PRange.UpwardEnumerable.mk.{u}

方法

succ? : α → Option α

将 α 中的元素映射到其后继；若不存在后继，则返回空值。

succMany? : Nat → α → Option α

将 α 中的元素映射到其第 n 个后继；若该后继不存在，则返回空值。这在语义上应表现得像重复应用 succ?，但可能更高效。

LawfulUpwardEnumerable 确保与 succ? 的兼容性。

如果在 UpwardEnumerable 实例中没有提供其他实现，succMany? 会重复应用 succ?。

定义

Std.PRange.UpwardEnumerable.LE.{u} {α : Type u}
  [Std.PRange.UpwardEnumerable α] (a b : α) : Prop
Std.PRange.UpwardEnumerable.LE.{u}
  {α : Type u}
  [Std.PRange.UpwardEnumerable α]
  (a b : α) : Prop

按照 UpwardEnumerable.LE，a 小于等于 b，当且仅当 b 等于 a 或是 a 的传递后继。

定义

Std.PRange.UpwardEnumerable.LT.{u} {α : Type u}
  [Std.PRange.UpwardEnumerable α] (a b : α) : Prop
Std.PRange.UpwardEnumerable.LT.{u}
  {α : Type u}
  [Std.PRange.UpwardEnumerable α]
  (a b : α) : Prop

按照 UpwardEnumerable.LT，a 小于 b，当且仅当 b 是 a 的真传递后继。“真”表示 b 是第 n 个后继，起点为 a，其中 n > 0。

给定 LawfulUpwardEnumerable α，α 中没有元素小于自身。

类型类

Std.PRange.LawfulUpwardEnumerable.{u} (α : Type u)
  [Std.PRange.UpwardEnumerable α] : Prop
Std.PRange.LawfulUpwardEnumerable.{u}
  (α : Type u)
  [Std.PRange.UpwardEnumerable α] : Prop

这种类型类确保 UpwardEnumerable α 实例行为良好。

实例构造子

Std.PRange.LawfulUpwardEnumerable.mk.{u}

方法

ne_of_lt : ∀ (a b : α), Std.PRange.UpwardEnumerable.LT a b → a ≠ b

后继链中不存在环。

succMany?_zero : ∀ (a : α), Std.PRange.succMany? 0 a = some a

0 阶后继对于 a 就是 a 自身。

succMany?_add_one : ∀ (n : Nat) (a : α), Std.PRange.succMany? (n + 1) a = (Std.PRange.succMany? n a).bind Std.PRange.succ?

n + 1 阶后继对于 a，等于其第 n 阶后继的后继，前提是这些后继确实存在。

类型类

Std.PRange.Least?.{u} (α : Type u) : Type u
Std.PRange.Least?.{u} (α : Type u) :
  Type u

类型类 Least? α 可选择性地提供 α、least? : Option α 的最小元素。

这种类型类的主要用例是将其与 UpwardEnumerable 结合使用，以获得 α 所有元素的（可能是无限的）升序枚举。

实例构造子

Std.PRange.Least?.mk.{u}

方法

least? : Option α

返回 α 中最小的元素；如果 α 为空，则返回空值。

仅允许空类型定义 least? := none。如果 α 有序且非空，则 least? 的值应为根据 α 上的顺序确定的最小元素。

类型类

Std.PRange.InfinitelyUpwardEnumerable.{u} (α : Type u)
  [Std.PRange.UpwardEnumerable α] : Prop
Std.PRange.InfinitelyUpwardEnumerable.{u}
  (α : Type u)
  [Std.PRange.UpwardEnumerable α] : Prop

这个命题类型类确保 UpwardEnumerable.succ? 永远不会返回 none。换句话说，它确保总是会有一个后继。

实例构造子

Std.PRange.InfinitelyUpwardEnumerable.mk.{u}

方法

isSome_succ? : ∀ (a : α), (Std.PRange.succ? a).isSome = true

α 的每个元素都有一个后继。

类型类

Std.PRange.LinearlyUpwardEnumerable.{u} (α : Type u)
  [Std.PRange.UpwardEnumerable α] : Prop
Std.PRange.LinearlyUpwardEnumerable.{u}
  (α : Type u)
  [Std.PRange.UpwardEnumerable α] : Prop

这个命题类型类确保 UpwardEnumerable.succ? 是单射的。

实例构造子

Std.PRange.LinearlyUpwardEnumerable.mk.{u}

方法

eq_of_succ?_eq : ∀ (a b : α), Std.PRange.succ? a = Std.PRange.succ? b → a = b

UpwardEnumerable.succ? 在 α 上的实现是单射函数。

类型类

Std.Rxi.IsAlwaysFinite.{u} (α : Type u)
  [Std.PRange.UpwardEnumerable α] : Prop
Std.Rxi.IsAlwaysFinite.{u} (α : Type u)
  [Std.PRange.UpwardEnumerable α] : Prop

这种类型类确保右无界的范围（即对于界 a、a...*、a<...* 和 *...*）总是有限的。这是许多函数和实例的前提条件，例如 Rci.toList 或 ForIn'。

实例构造子

Std.Rxi.IsAlwaysFinite.mk.{u}

方法

finite : ∀ (init : α), ∃ n, Std.PRange.succMany? n init = none

对于每个元素 init，存在一个后继链，最终得到一个没有后继的元素。

类型类

Std.Rxi.HasSize.{u} (α : Type u) : Type u
Std.Rxi.HasSize.{u} (α : Type u) : Type u

此类型类为下界无界的区间（Ric.size、Rio.size 和 Rii.size）提供大小函数。

返回的大小应等于 toList 返回的元素数量。此条件由类型类 LawfulHasSize 描述。

实例构造子

Std.Rxi.HasSize.mk.{u}

方法

size : α → Nat

返回从 lo 开始满足给定上限的元素数量。

类型类

Std.Rxc.IsAlwaysFinite.{u} (α : Type u) [Std.PRange.UpwardEnumerable α]
  [LE α] : Prop
Std.Rxc.IsAlwaysFinite.{u} (α : Type u)
  [Std.PRange.UpwardEnumerable α] [LE α] :
  Prop

此类型类确保右闭区间（即，对边界 a 和 b 而言，a...=b、a<...=b 与 *...=b）总是有限。这是 Rcc.toList、ForIn' 等许多函数和实例的前提。

实例构造子

Std.Rxc.IsAlwaysFinite.mk.{u}

方法

finite : ∀ (init hi : α), ∃ n, (Std.PRange.succMany? n init).elim True fun x => ¬x ≤ hi

对于每一对元素 init 和 hi，存在一个后继链，最终得到一个要么没有后继要么大于 hi 的元素。

类型类

Std.Rxc.HasSize.{u} (α : Type u) : Type u
Std.Rxc.HasSize.{u} (α : Type u) : Type u

此类型类为具有闭下界的区间（Rcc.size、Rco.size 和 Rci.size）提供大小函数。

返回的大小应等于 toList 返回的元素数量。此条件由类型类 LawfulHasSize 描述。

实例构造子

Std.Rxc.HasSize.mk.{u}

方法

size : α → α → Nat

返回从 lo 开始满足给定上限的元素数量。

20.18.3. 实现范围🔗

内置范围类型可以与任何类型一起使用，但它们的实用性取决于某些类型类实例的存在。一般来说，范围要么被检查成员资格，要么被枚举或迭代。为了检查一个值是否包含在范围内，使用 DecidableLT 和 DecidableLE 实例来将该值与范围各自的开、闭端点进行比较。要获取范围的迭代器，只需要 Std.PRange.UpwardEnumerable 和 Std.PRange.LawfulUpwardEnumerable 的实例。为了在 Lean.Parser.Term.doFor : doElemfor 循环中直接对其进行迭代，还需要 Std.PRange.LawfulUpwardEnumerableLE 和 Std.PRange.LawfulUpwardEnumerableLT。为了枚举一个范围（例如，通过调用 toList），必须证明它是有限的。这是通过提供 Std.Rxi.IsAlwaysFinite、Std.Rxc.IsAlwaysFinite 或 Std.Rxo.IsAlwaysFinite 的实例来完成的。

实现范围

枚举类型 Day 表示一周中的每一天：

inductive Day where
  | mo | tu | we | th | fr | sa | su
deriving Repr

虽然在范围中使用这种类型已经是可能的，但它们并不是特别有用。没有成员资格实例：

#eval failed to synthesize instance of type class
  Membership Day (Std.Rcc Day)

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.Day.we ∈ (Day.mo...=Day.fr)

failed to synthesize instance of type class
  Membership Day (Std.Rcc Day)

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.

范围不能被迭代：

#eval show IO Unit from
  failed to synthesize instance of type class
  ForIn IO (Std.Rcc Day) ?α

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.for d in Day.mo...=Day.fr do
    IO.println s!"It's {repr d}"

failed to synthesize instance of type class
  ForIn IO (Std.Rcc Day) ?α

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.

也不能枚举它们，即使该类型是有限的：

#eval failed to synthesize instance of type class
  Std.PRange.UpwardEnumerable Day

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.(Day.sa...*).toList

failed to synthesize instance of type class
  Std.PRange.UpwardEnumerable Day

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.

成员资格测试需要 DecidableLT 和 DecidableLE 实例。获取它们的简单方法是为每一天编号，然后比较数字：

def Day.toNat : Day → Nat
  | mo => 0
  | tu => 1
  | we => 2
  | th => 3
  | fr => 4
  | sa => 5
  | su => 6

instance : LT Day where
  lt d1 d2 := d1.toNat < d2.toNat

instance : LE Day where
  le d1 d2 := d1.toNat ≤ d2.toNat

instance : DecidableLT Day :=
  fun d1 d2 => inferInstanceAs (Decidable (d1.toNat < d2.toNat))

instance : DecidableLE Day :=
  fun d1 d2 => inferInstanceAs (Decidable (d1.toNat ≤ d2.toNat))

有了这些实例，成员资格测试将如预期般工作：

def Day.isWeekday (d : Day) : Bool := d ∈ Day.mo...Day.sa

true#eval Day.th.isWeekday

true

false#eval Day.sa.isWeekday

false

迭代和枚举都是重复应用后继函数的变体，直到达到范围的上界或该类型的最大元素。该后继函数是 Std.PRange.UpwardEnumerable.succ?。在 Day 的命名空间中定义该函数以与广义字段表示法一起使用也很方便：

def Day.succ? : Day → Option Day
  | mo => some tu
  | tu => some we
  | we => some th
  | th => some fr
  | fr => some sa
  | sa => some su
  | su => none

instance : Std.PRange.UpwardEnumerable Day where
  succ? := Day.succ?

迭代还需要证明 succ? 的实现是合理的。其属性根据 Std.PRange.UpwardEnumerable.succMany? 来表达，它迭代应用 succ? 若干次，并基于 Nat.repeat 和 succ? 具有默认实现。特别地，LawfulUpwardEnumerable 实例需要证明 Std.PRange.UpwardEnumerable.succMany? 与默认实现相对应，同时证明重复应用后继函数永远不会再次产生相同的元素。

第一步是为关于 succMany? 的两个证明编写两个辅助引理。虽然它们可以内联在实例声明中编写，但为了方便起见，可以让它们具有 @[simp] 属性。

@[simp]
theorem Day.succMany?_zero (d : Day) :
  Std.PRange.succMany? 0 d = some d := byd:Day⊢ Std.PRange.succMany? 0 d = some d
  simp [Std.PRange.succMany?, Nat.repeat]All goals completed! 🐙

@[simp]
theorem Day.succMany?_add_one (n : Nat) (d : Day) :
    Std.PRange.succMany? (n + 1) d =
    (Std.PRange.succMany? n d).bind Std.PRange.succ? := byn:Natd:Day⊢ Std.PRange.succMany? (n + 1) d = (Std.PRange.succMany? n d).bind Std.PRange.succ?
  simp [Std.PRange.succMany?, Nat.repeat, Std.PRange.succ?]All goals completed! 🐙

证明后继函数中没有循环，需要使用一个方便的辅助引理，该引理可以计算任意两天之间的后继步数。它被标记为 @[grind →]，因为当存在与其前提相匹配的假设时，它会添加大量的新信息：

@[grind →]
theorem Day.succMany?_steps {d d' : Day} {steps} :
    Std.PRange.succMany? steps d = some d' →
    if d ≤ d' then steps = d'.toNat - d.toNat
    else False := byd:Dayd':Daysteps:Nat⊢ Std.PRange.succMany? steps d = some d' → if d ≤ d' then steps = d'.toNat - d.toNat else False
  intro hd:Dayd':Daysteps:Nath:Std.PRange.succMany? steps d = some d'⊢ if d ≤ d' then steps = d'.toNat - d.toNat else False
  match steps with
  | 0 | 1 | 2 | 3 | 4 | 5 | 6 =>d:Dayd':Daysteps:Nath:Std.PRange.succMany? 6 d = some d'⊢ if d ≤ d' then 6 = d'.toNat - d.toNat else Falsed:Dayd':Daysteps:Nath:Std.PRange.succMany? 5 d = some d'⊢ if d ≤ d' then 5 = d'.toNat - d.toNat else Falsed:Dayd':Daysteps:Nath:Std.PRange.succMany? 4 d = some d'⊢ if d ≤ d' then 4 = d'.toNat - d.toNat else Falsed:Dayd':Daysteps:Nath:Std.PRange.succMany? 3 d = some d'⊢ if d ≤ d' then 3 = d'.toNat - d.toNat else Falsed:Dayd':Daysteps:Nath:Std.PRange.succMany? 2 d = some d'⊢ if d ≤ d' then 2 = d'.toNat - d.toNat else Falsed:Dayd':Daysteps:Nath:Std.PRange.succMany? 1 d = some d'⊢ if d ≤ d' then 1 = d'.toNat - d.toNat else Falsed:Dayd':Daysteps:Nath:Std.PRange.succMany? 0 d = some d'⊢ if d ≤ d' then 0 = d'.toNat - d.toNat else False
    cases dmod':Daysteps:Nath:Std.PRange.succMany? 6 mo = some d'⊢ if mo ≤ d' then 6 = d'.toNat - mo.toNat else Falsetud':Daysteps:Nath:Std.PRange.succMany? 6 tu = some d'⊢ if tu ≤ d' then 6 = d'.toNat - tu.toNat else Falsewed':Daysteps:Nath:Std.PRange.succMany? 6 we = some d'⊢ if we ≤ d' then 6 = d'.toNat - we.toNat else Falsethd':Daysteps:Nath:Std.PRange.succMany? 6 th = some d'⊢ if th ≤ d' then 6 = d'.toNat - th.toNat else Falsefrd':Daysteps:Nath:Std.PRange.succMany? 6 fr = some d'⊢ if fr ≤ d' then 6 = d'.toNat - fr.toNat else Falsesad':Daysteps:Nath:Std.PRange.succMany? 6 sa = some d'⊢ if sa ≤ d' then 6 = d'.toNat - sa.toNat else Falsesud':Daysteps:Nath:Std.PRange.succMany? 6 su = some d'⊢ if su ≤ d' then 6 = d'.toNat - su.toNat else False <;>mod':Daysteps:Nath:Std.PRange.succMany? 6 mo = some d'⊢ if mo ≤ d' then 6 = d'.toNat - mo.toNat else Falsetud':Daysteps:Nath:Std.PRange.succMany? 6 tu = some d'⊢ if tu ≤ d' then 6 = d'.toNat - tu.toNat else Falsewed':Daysteps:Nath:Std.PRange.succMany? 6 we = some d'⊢ if we ≤ d' then 6 = d'.toNat - we.toNat else Falsethd':Daysteps:Nath:Std.PRange.succMany? 6 th = some d'⊢ if th ≤ d' then 6 = d'.toNat - th.toNat else Falsefrd':Daysteps:Nath:Std.PRange.succMany? 6 fr = some d'⊢ if fr ≤ d' then 6 = d'.toNat - fr.toNat else Falsesad':Daysteps:Nath:Std.PRange.succMany? 6 sa = some d'⊢ if sa ≤ d' then 6 = d'.toNat - sa.toNat else Falsesud':Daysteps:Nath:Std.PRange.succMany? 6 su = some d'⊢ if su ≤ d' then 6 = d'.toNat - su.toNat else False cases d'su.mosteps:Nath:Std.PRange.succMany? 6 su = some mo⊢ if su ≤ mo then 6 = mo.toNat - su.toNat else Falsesu.tusteps:Nath:Std.PRange.succMany? 6 su = some tu⊢ if su ≤ tu then 6 = tu.toNat - su.toNat else Falsesu.westeps:Nath:Std.PRange.succMany? 6 su = some we⊢ if su ≤ we then 6 = we.toNat - su.toNat else Falsesu.thsteps:Nath:Std.PRange.succMany? 6 su = some th⊢ if su ≤ th then 6 = th.toNat - su.toNat else Falsesu.frsteps:Nath:Std.PRange.succMany? 6 su = some fr⊢ if su ≤ fr then 6 = fr.toNat - su.toNat else Falsesu.sasteps:Nath:Std.PRange.succMany? 6 su = some sa⊢ if su ≤ sa then 6 = sa.toNat - su.toNat else Falsesu.susteps:Nath:Std.PRange.succMany? 6 su = some su⊢ if su ≤ su then 6 = su.toNat - su.toNat else False <;>mo.mosteps:Nath:Std.PRange.succMany? 6 mo = some mo⊢ if mo ≤ mo then 6 = mo.toNat - mo.toNat else Falsemo.tusteps:Nath:Std.PRange.succMany? 6 mo = some tu⊢ if mo ≤ tu then 6 = tu.toNat - mo.toNat else Falsemo.westeps:Nath:Std.PRange.succMany? 6 mo = some we⊢ if mo ≤ we then 6 = we.toNat - mo.toNat else Falsemo.thsteps:Nath:Std.PRange.succMany? 6 mo = some th⊢ if mo ≤ th then 6 = th.toNat - mo.toNat else Falsemo.frsteps:Nath:Std.PRange.succMany? 6 mo = some fr⊢ if mo ≤ fr then 6 = fr.toNat - mo.toNat else Falsemo.sasteps:Nath:Std.PRange.succMany? 6 mo = some sa⊢ if mo ≤ sa then 6 = sa.toNat - mo.toNat else Falsemo.susteps:Nath:Std.PRange.succMany? 6 mo = some su⊢ if mo ≤ su then 6 = su.toNat - mo.toNat else Falsetu.mosteps:Nath:Std.PRange.succMany? 6 tu = some mo⊢ if tu ≤ mo then 6 = mo.toNat - tu.toNat else Falsetu.tusteps:Nath:Std.PRange.succMany? 6 tu = some tu⊢ if tu ≤ tu then 6 = tu.toNat - tu.toNat else Falsetu.westeps:Nath:Std.PRange.succMany? 6 tu = some we⊢ if tu ≤ we then 6 = we.toNat - tu.toNat else Falsetu.thsteps:Nath:Std.PRange.succMany? 6 tu = some th⊢ if tu ≤ th then 6 = th.toNat - tu.toNat else Falsetu.frsteps:Nath:Std.PRange.succMany? 6 tu = some fr⊢ if tu ≤ fr then 6 = fr.toNat - tu.toNat else Falsetu.sasteps:Nath:Std.PRange.succMany? 6 tu = some sa⊢ if tu ≤ sa then 6 = sa.toNat - tu.toNat else Falsetu.susteps:Nath:Std.PRange.succMany? 6 tu = some su⊢ if tu ≤ su then 6 = su.toNat - tu.toNat else Falsewe.mosteps:Nath:Std.PRange.succMany? 6 we = some mo⊢ if we ≤ mo then 6 = mo.toNat - we.toNat else Falsewe.tusteps:Nath:Std.PRange.succMany? 6 we = some tu⊢ if we ≤ tu then 6 = tu.toNat - we.toNat else Falsewe.westeps:Nath:Std.PRange.succMany? 6 we = some we⊢ if we ≤ we then 6 = we.toNat - we.toNat else Falsewe.thsteps:Nath:Std.PRange.succMany? 6 we = some th⊢ if we ≤ th then 6 = th.toNat - we.toNat else Falsewe.frsteps:Nath:Std.PRange.succMany? 6 we = some fr⊢ if we ≤ fr then 6 = fr.toNat - we.toNat else Falsewe.sasteps:Nath:Std.PRange.succMany? 6 we = some sa⊢ if we ≤ sa then 6 = sa.toNat - we.toNat else Falsewe.susteps:Nath:Std.PRange.succMany? 6 we = some su⊢ if we ≤ su then 6 = su.toNat - we.toNat else Falseth.mosteps:Nath:Std.PRange.succMany? 6 th = some mo⊢ if th ≤ mo then 6 = mo.toNat - th.toNat else Falseth.tusteps:Nath:Std.PRange.succMany? 6 th = some tu⊢ if th ≤ tu then 6 = tu.toNat - th.toNat else Falseth.westeps:Nath:Std.PRange.succMany? 6 th = some we⊢ if th ≤ we then 6 = we.toNat - th.toNat else Falseth.thsteps:Nath:Std.PRange.succMany? 6 th = some th⊢ if th ≤ th then 6 = th.toNat - th.toNat else Falseth.frsteps:Nath:Std.PRange.succMany? 6 th = some fr⊢ if th ≤ fr then 6 = fr.toNat - th.toNat else Falseth.sasteps:Nath:Std.PRange.succMany? 6 th = some sa⊢ if th ≤ sa then 6 = sa.toNat - th.toNat else Falseth.susteps:Nath:Std.PRange.succMany? 6 th = some su⊢ if th ≤ su then 6 = su.toNat - th.toNat else Falsefr.mosteps:Nath:Std.PRange.succMany? 6 fr = some mo⊢ if fr ≤ mo then 6 = mo.toNat - fr.toNat else Falsefr.tusteps:Nath:Std.PRange.succMany? 6 fr = some tu⊢ if fr ≤ tu then 6 = tu.toNat - fr.toNat else Falsefr.westeps:Nath:Std.PRange.succMany? 6 fr = some we⊢ if fr ≤ we then 6 = we.toNat - fr.toNat else Falsefr.thsteps:Nath:Std.PRange.succMany? 6 fr = some th⊢ if fr ≤ th then 6 = th.toNat - fr.toNat else Falsefr.frsteps:Nath:Std.PRange.succMany? 6 fr = some fr⊢ if fr ≤ fr then 6 = fr.toNat - fr.toNat else Falsefr.sasteps:Nath:Std.PRange.succMany? 6 fr = some sa⊢ if fr ≤ sa then 6 = sa.toNat - fr.toNat else Falsefr.susteps:Nath:Std.PRange.succMany? 6 fr = some su⊢ if fr ≤ su then 6 = su.toNat - fr.toNat else Falsesa.mosteps:Nath:Std.PRange.succMany? 6 sa = some mo⊢ if sa ≤ mo then 6 = mo.toNat - sa.toNat else Falsesa.tusteps:Nath:Std.PRange.succMany? 6 sa = some tu⊢ if sa ≤ tu then 6 = tu.toNat - sa.toNat else Falsesa.westeps:Nath:Std.PRange.succMany? 6 sa = some we⊢ if sa ≤ we then 6 = we.toNat - sa.toNat else Falsesa.thsteps:Nath:Std.PRange.succMany? 6 sa = some th⊢ if sa ≤ th then 6 = th.toNat - sa.toNat else Falsesa.frsteps:Nath:Std.PRange.succMany? 6 sa = some fr⊢ if sa ≤ fr then 6 = fr.toNat - sa.toNat else Falsesa.sasteps:Nath:Std.PRange.succMany? 6 sa = some sa⊢ if sa ≤ sa then 6 = sa.toNat - sa.toNat else Falsesa.susteps:Nath:Std.PRange.succMany? 6 sa = some su⊢ if sa ≤ su then 6 = su.toNat - sa.toNat else Falsesu.mosteps:Nath:Std.PRange.succMany? 6 su = some mo⊢ if su ≤ mo then 6 = mo.toNat - su.toNat else Falsesu.tusteps:Nath:Std.PRange.succMany? 6 su = some tu⊢ if su ≤ tu then 6 = tu.toNat - su.toNat else Falsesu.westeps:Nath:Std.PRange.succMany? 6 su = some we⊢ if su ≤ we then 6 = we.toNat - su.toNat else Falsesu.thsteps:Nath:Std.PRange.succMany? 6 su = some th⊢ if su ≤ th then 6 = th.toNat - su.toNat else Falsesu.frsteps:Nath:Std.PRange.succMany? 6 su = some fr⊢ if su ≤ fr then 6 = fr.toNat - su.toNat else Falsesu.sasteps:Nath:Std.PRange.succMany? 6 su = some sa⊢ if su ≤ sa then 6 = sa.toNat - su.toNat else Falsesu.susteps:Nath:Std.PRange.succMany? 6 su = some su⊢ if su ≤ su then 6 = su.toNat - su.toNat else False
    simp_all +decide [Std.PRange.succMany?, Nat.repeat, Day.succ?]All goals completed! 🐙
  | n + 7 =>d:Dayd':Daysteps:Natn:Nath:Std.PRange.succMany? (n + 7) d = some d'⊢ if d ≤ d' then n + 7 = d'.toNat - d.toNat else False
    simp at hd:Dayd':Daysteps:Natn:Nath:(((((((Std.PRange.succMany? n d).bind Std.PRange.succ?).bind Std.PRange.succ?).bind Std.PRange.succ?).bind
                Std.PRange.succ?).bind
            Std.PRange.succ?).bind
        Std.PRange.succ?).bind
    Std.PRange.succ? =
  some d'⊢ if d ≤ d' then n + 7 = d'.toNat - d.toNat else False
    cases h' : (Std.PRange.succMany? n d) with
    | none =>noned:Dayd':Daysteps:Natn:Nath:(((((((Std.PRange.succMany? n d).bind Std.PRange.succ?).bind Std.PRange.succ?).bind Std.PRange.succ?).bind
                Std.PRange.succ?).bind
            Std.PRange.succ?).bind
        Std.PRange.succ?).bind
    Std.PRange.succ? =
  some d'h':Std.PRange.succMany? n d = none⊢ if d ≤ d' then n + 7 = d'.toNat - d.toNat else False
      simp_allAll goals completed! 🐙
    | some d'' =>somed:Dayd':Daysteps:Natn:Nath:(((((((Std.PRange.succMany? n d).bind Std.PRange.succ?).bind Std.PRange.succ?).bind Std.PRange.succ?).bind
                Std.PRange.succ?).bind
            Std.PRange.succ?).bind
        Std.PRange.succ?).bind
    Std.PRange.succ? =
  some d'd'':Dayh':Std.PRange.succMany? n d = some d''⊢ if d ≤ d' then n + 7 = d'.toNat - d.toNat else False
      rw [h'somed:Dayd':Daysteps:Natn:Natd'':Dayh:(((((((some d'').bind Std.PRange.succ?).bind Std.PRange.succ?).bind Std.PRange.succ?).bind Std.PRange.succ?).bind
            Std.PRange.succ?).bind
        Std.PRange.succ?).bind
    Std.PRange.succ? =
  some d'h':Std.PRange.succMany? n d = some d''⊢ if d ≤ d' then n + 7 = d'.toNat - d.toNat else False] at hsomed:Dayd':Daysteps:Natn:Natd'':Dayh:(((((((some d'').bind Std.PRange.succ?).bind Std.PRange.succ?).bind Std.PRange.succ?).bind Std.PRange.succ?).bind
            Std.PRange.succ?).bind
        Std.PRange.succ?).bind
    Std.PRange.succ? =
  some d'h':Std.PRange.succMany? n d = some d''⊢ if d ≤ d' then n + 7 = d'.toNat - d.toNat else False
      cases d''some.mod:Dayd':Daysteps:Natn:Nath:(((((((some mo).bind Std.PRange.succ?).bind Std.PRange.succ?).bind Std.PRange.succ?).bind Std.PRange.succ?).bind
            Std.PRange.succ?).bind
        Std.PRange.succ?).bind
    Std.PRange.succ? =
  some d'h':Std.PRange.succMany? n d = some mo⊢ if d ≤ d' then n + 7 = d'.toNat - d.toNat else Falsesome.tud:Dayd':Daysteps:Natn:Nath:(((((((some tu).bind Std.PRange.succ?).bind Std.PRange.succ?).bind Std.PRange.succ?).bind Std.PRange.succ?).bind
            Std.PRange.succ?).bind
        Std.PRange.succ?).bind
    Std.PRange.succ? =
  some d'h':Std.PRange.succMany? n d = some tu⊢ if d ≤ d' then n + 7 = d'.toNat - d.toNat else Falsesome.wed:Dayd':Daysteps:Natn:Nath:(((((((some we).bind Std.PRange.succ?).bind Std.PRange.succ?).bind Std.PRange.succ?).bind Std.PRange.succ?).bind
            Std.PRange.succ?).bind
        Std.PRange.succ?).bind
    Std.PRange.succ? =
  some d'h':Std.PRange.succMany? n d = some we⊢ if d ≤ d' then n + 7 = d'.toNat - d.toNat else Falsesome.thd:Dayd':Daysteps:Natn:Nath:(((((((some th).bind Std.PRange.succ?).bind Std.PRange.succ?).bind Std.PRange.succ?).bind Std.PRange.succ?).bind
            Std.PRange.succ?).bind
        Std.PRange.succ?).bind
    Std.PRange.succ? =
  some d'h':Std.PRange.succMany? n d = some th⊢ if d ≤ d' then n + 7 = d'.toNat - d.toNat else Falsesome.frd:Dayd':Daysteps:Natn:Nath:(((((((some fr).bind Std.PRange.succ?).bind Std.PRange.succ?).bind Std.PRange.succ?).bind Std.PRange.succ?).bind
            Std.PRange.succ?).bind
        Std.PRange.succ?).bind
    Std.PRange.succ? =
  some d'h':Std.PRange.succMany? n d = some fr⊢ if d ≤ d' then n + 7 = d'.toNat - d.toNat else Falsesome.sad:Dayd':Daysteps:Natn:Nath:(((((((some sa).bind Std.PRange.succ?).bind Std.PRange.succ?).bind Std.PRange.succ?).bind Std.PRange.succ?).bind
            Std.PRange.succ?).bind
        Std.PRange.succ?).bind
    Std.PRange.succ? =
  some d'h':Std.PRange.succMany? n d = some sa⊢ if d ≤ d' then n + 7 = d'.toNat - d.toNat else Falsesome.sud:Dayd':Daysteps:Natn:Nath:(((((((some su).bind Std.PRange.succ?).bind Std.PRange.succ?).bind Std.PRange.succ?).bind Std.PRange.succ?).bind
            Std.PRange.succ?).bind
        Std.PRange.succ?).bind
    Std.PRange.succ? =
  some d'h':Std.PRange.succMany? n d = some su⊢ if d ≤ d' then n + 7 = d'.toNat - d.toNat else False <;>some.mod:Dayd':Daysteps:Natn:Nath:(((((((some mo).bind Std.PRange.succ?).bind Std.PRange.succ?).bind Std.PRange.succ?).bind Std.PRange.succ?).bind
            Std.PRange.succ?).bind
        Std.PRange.succ?).bind
    Std.PRange.succ? =
  some d'h':Std.PRange.succMany? n d = some mo⊢ if d ≤ d' then n + 7 = d'.toNat - d.toNat else Falsesome.tud:Dayd':Daysteps:Natn:Nath:(((((((some tu).bind Std.PRange.succ?).bind Std.PRange.succ?).bind Std.PRange.succ?).bind Std.PRange.succ?).bind
            Std.PRange.succ?).bind
        Std.PRange.succ?).bind
    Std.PRange.succ? =
  some d'h':Std.PRange.succMany? n d = some tu⊢ if d ≤ d' then n + 7 = d'.toNat - d.toNat else Falsesome.wed:Dayd':Daysteps:Natn:Nath:(((((((some we).bind Std.PRange.succ?).bind Std.PRange.succ?).bind Std.PRange.succ?).bind Std.PRange.succ?).bind
            Std.PRange.succ?).bind
        Std.PRange.succ?).bind
    Std.PRange.succ? =
  some d'h':Std.PRange.succMany? n d = some we⊢ if d ≤ d' then n + 7 = d'.toNat - d.toNat else Falsesome.thd:Dayd':Daysteps:Natn:Nath:(((((((some th).bind Std.PRange.succ?).bind Std.PRange.succ?).bind Std.PRange.succ?).bind Std.PRange.succ?).bind
            Std.PRange.succ?).bind
        Std.PRange.succ?).bind
    Std.PRange.succ? =
  some d'h':Std.PRange.succMany? n d = some th⊢ if d ≤ d' then n + 7 = d'.toNat - d.toNat else Falsesome.frd:Dayd':Daysteps:Natn:Nath:(((((((some fr).bind Std.PRange.succ?).bind Std.PRange.succ?).bind Std.PRange.succ?).bind Std.PRange.succ?).bind
            Std.PRange.succ?).bind
        Std.PRange.succ?).bind
    Std.PRange.succ? =
  some d'h':Std.PRange.succMany? n d = some fr⊢ if d ≤ d' then n + 7 = d'.toNat - d.toNat else Falsesome.sad:Dayd':Daysteps:Natn:Nath:(((((((some sa).bind Std.PRange.succ?).bind Std.PRange.succ?).bind Std.PRange.succ?).bind Std.PRange.succ?).bind
            Std.PRange.succ?).bind
        Std.PRange.succ?).bind
    Std.PRange.succ? =
  some d'h':Std.PRange.succMany? n d = some sa⊢ if d ≤ d' then n + 7 = d'.toNat - d.toNat else Falsesome.sud:Dayd':Daysteps:Natn:Nath:(((((((some su).bind Std.PRange.succ?).bind Std.PRange.succ?).bind Std.PRange.succ?).bind Std.PRange.succ?).bind
            Std.PRange.succ?).bind
        Std.PRange.succ?).bind
    Std.PRange.succ? =
  some d'h':Std.PRange.succMany? n d = some su⊢ if d ≤ d' then n + 7 = d'.toNat - d.toNat else False contradictionAll goals completed! 🐙

有了这个辅助引理，证明就非常简短了：

instance : Std.PRange.LawfulUpwardEnumerable Day where
  ne_of_lt d1 d2 h := byd1:Dayd2:Dayh:Std.PRange.UpwardEnumerable.LT d1 d2⊢ d1 ≠ d2 grind [Std.PRange.UpwardEnumerable.LT]All goals completed! 🐙
  succMany?_zero := Day.succMany?_zero
  succMany?_add_one := Day.succMany?_add_one

证明三种可枚举范围是有限的，使得枚举天数范围成为可能：

instance : Std.Rxo.IsAlwaysFinite Day where
  finite init hi :=
    ⟨7, byinit:Dayhi:Day⊢ (Std.PRange.succMany? 7 init).elim True fun x => ¬x < hi cases initmohi:Day⊢ (Std.PRange.succMany? 7 Day.mo).elim True fun x => ¬x < hituhi:Day⊢ (Std.PRange.succMany? 7 Day.tu).elim True fun x => ¬x < hiwehi:Day⊢ (Std.PRange.succMany? 7 Day.we).elim True fun x => ¬x < hithhi:Day⊢ (Std.PRange.succMany? 7 Day.th).elim True fun x => ¬x < hifrhi:Day⊢ (Std.PRange.succMany? 7 Day.fr).elim True fun x => ¬x < hisahi:Day⊢ (Std.PRange.succMany? 7 Day.sa).elim True fun x => ¬x < hisuhi:Day⊢ (Std.PRange.succMany? 7 Day.su).elim True fun x => ¬x < hi <;>mohi:Day⊢ (Std.PRange.succMany? 7 Day.mo).elim True fun x => ¬x < hituhi:Day⊢ (Std.PRange.succMany? 7 Day.tu).elim True fun x => ¬x < hiwehi:Day⊢ (Std.PRange.succMany? 7 Day.we).elim True fun x => ¬x < hithhi:Day⊢ (Std.PRange.succMany? 7 Day.th).elim True fun x => ¬x < hifrhi:Day⊢ (Std.PRange.succMany? 7 Day.fr).elim True fun x => ¬x < hisahi:Day⊢ (Std.PRange.succMany? 7 Day.sa).elim True fun x => ¬x < hisuhi:Day⊢ (Std.PRange.succMany? 7 Day.su).elim True fun x => ¬x < hi simp [Std.PRange.succ?, Day.succ?]All goals completed! 🐙⟩

instance : Std.Rxc.IsAlwaysFinite Day where
  finite init hi :=
    ⟨7, byinit:Dayhi:Day⊢ (Std.PRange.succMany? 7 init).elim True fun x => ¬x ≤ hi cases initmohi:Day⊢ (Std.PRange.succMany? 7 Day.mo).elim True fun x => ¬x ≤ hituhi:Day⊢ (Std.PRange.succMany? 7 Day.tu).elim True fun x => ¬x ≤ hiwehi:Day⊢ (Std.PRange.succMany? 7 Day.we).elim True fun x => ¬x ≤ hithhi:Day⊢ (Std.PRange.succMany? 7 Day.th).elim True fun x => ¬x ≤ hifrhi:Day⊢ (Std.PRange.succMany? 7 Day.fr).elim True fun x => ¬x ≤ hisahi:Day⊢ (Std.PRange.succMany? 7 Day.sa).elim True fun x => ¬x ≤ hisuhi:Day⊢ (Std.PRange.succMany? 7 Day.su).elim True fun x => ¬x ≤ hi <;>mohi:Day⊢ (Std.PRange.succMany? 7 Day.mo).elim True fun x => ¬x ≤ hituhi:Day⊢ (Std.PRange.succMany? 7 Day.tu).elim True fun x => ¬x ≤ hiwehi:Day⊢ (Std.PRange.succMany? 7 Day.we).elim True fun x => ¬x ≤ hithhi:Day⊢ (Std.PRange.succMany? 7 Day.th).elim True fun x => ¬x ≤ hifrhi:Day⊢ (Std.PRange.succMany? 7 Day.fr).elim True fun x => ¬x ≤ hisahi:Day⊢ (Std.PRange.succMany? 7 Day.sa).elim True fun x => ¬x ≤ hisuhi:Day⊢ (Std.PRange.succMany? 7 Day.su).elim True fun x => ¬x ≤ hi simp [Std.PRange.succ?, Day.succ?]All goals completed! 🐙⟩

instance : Std.Rxi.IsAlwaysFinite Day where
  finite init := ⟨7, byinit:Day⊢ Std.PRange.succMany? 7 init = none cases initmo⊢ Std.PRange.succMany? 7 Day.mo = nonetu⊢ Std.PRange.succMany? 7 Day.tu = nonewe⊢ Std.PRange.succMany? 7 Day.we = noneth⊢ Std.PRange.succMany? 7 Day.th = nonefr⊢ Std.PRange.succMany? 7 Day.fr = nonesa⊢ Std.PRange.succMany? 7 Day.sa = nonesu⊢ Std.PRange.succMany? 7 Day.su = none <;>mo⊢ Std.PRange.succMany? 7 Day.mo = nonetu⊢ Std.PRange.succMany? 7 Day.tu = nonewe⊢ Std.PRange.succMany? 7 Day.we = noneth⊢ Std.PRange.succMany? 7 Day.th = nonefr⊢ Std.PRange.succMany? 7 Day.fr = nonesa⊢ Std.PRange.succMany? 7 Day.sa = nonesu⊢ Std.PRange.succMany? 7 Day.su = none rflAll goals completed! 🐙⟩

def allWeekdays : List Day := (Day.mo...Day.sa).toList
[Day.mo, Day.tu, Day.we, Day.th, Day.fr]#eval allWeekdays

[Day.mo, Day.tu, Day.we, Day.th, Day.fr]

添加 Std.PRange.Least? 实例允许枚举左无界范围：

instance : Std.PRange.Least? Day where
  least? := some .mo

def allWeekdays' : List Day := (*...Day.sa).toList
[Day.mo, Day.tu, Day.we, Day.th, Day.fr]#eval allWeekdays'

[Day.mo, Day.tu, Day.we, Day.th, Day.fr]

也可以创建一个可以枚举的迭代器，但它还不能与 Lean.Parser.Term.doFor : doElemfor 一起使用：

[Day.we, Day.th]#eval (Day.we...Day.fr).iter.toList

[Day.we, Day.th]

#eval show IO Unit from do
  failed to synthesize instance of type class
  ForIn IO (Std.Iter Day) ?α

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.for d in (Day.mo...Day.th).iter do
    IO.println s!"It's {repr d}."

failed to synthesize instance of type class
  ForIn IO (Std.Iter Day) ?α

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.

启用迭代，从而使天的范围功能完备的最后一步是证明在 Day 上的小于和小于等于关系对应于由迭代后继函数导出的不等式概念。这被捕获在类 Std.PRange.LawfulUpwardEnumerableLT 和 Std.PRange.LawfulUpwardEnumerableLE 中，它们要求这两个概念在逻辑上是等价的：

instance : Std.PRange.LawfulUpwardEnumerableLT Day where
  lt_iff d1 d2 := byd1:Dayd2:Day⊢ d1 < d2 ↔ Std.PRange.UpwardEnumerable.LT d1 d2
    constructormpd1:Dayd2:Day⊢ d1 < d2 → Std.PRange.UpwardEnumerable.LT d1 d2mprd1:Dayd2:Day⊢ Std.PRange.UpwardEnumerable.LT d1 d2 → d1 < d2
    .mpd1:Dayd2:Day⊢ d1 < d2 → Std.PRange.UpwardEnumerable.LT d1 d2 intro ltmpd1:Dayd2:Daylt:d1 < d2⊢ Std.PRange.UpwardEnumerable.LT d1 d2
      simp only [Std.PRange.UpwardEnumerable.LT, Day.succMany?_add_one]mpd1:Dayd2:Daylt:d1 < d2⊢ ∃ n, (Std.PRange.succMany? n d1).bind Std.PRange.succ? = some d2
      exists d2.toNat - d1.toNat.succmpd1:Dayd2:Daylt:d1 < d2⊢ (Std.PRange.succMany? (d2.toNat - d1.toNat.succ) d1).bind Std.PRange.succ? = some d2
      cases d1mp.mod2:Daylt:Day.mo < d2⊢ (Std.PRange.succMany? (d2.toNat - Day.mo.toNat.succ) Day.mo).bind Std.PRange.succ? = some d2mp.tud2:Daylt:Day.tu < d2⊢ (Std.PRange.succMany? (d2.toNat - Day.tu.toNat.succ) Day.tu).bind Std.PRange.succ? = some d2mp.wed2:Daylt:Day.we < d2⊢ (Std.PRange.succMany? (d2.toNat - Day.we.toNat.succ) Day.we).bind Std.PRange.succ? = some d2mp.thd2:Daylt:Day.th < d2⊢ (Std.PRange.succMany? (d2.toNat - Day.th.toNat.succ) Day.th).bind Std.PRange.succ? = some d2mp.frd2:Daylt:Day.fr < d2⊢ (Std.PRange.succMany? (d2.toNat - Day.fr.toNat.succ) Day.fr).bind Std.PRange.succ? = some d2mp.sad2:Daylt:Day.sa < d2⊢ (Std.PRange.succMany? (d2.toNat - Day.sa.toNat.succ) Day.sa).bind Std.PRange.succ? = some d2mp.sud2:Daylt:Day.su < d2⊢ (Std.PRange.succMany? (d2.toNat - Day.su.toNat.succ) Day.su).bind Std.PRange.succ? = some d2 <;>mp.mod2:Daylt:Day.mo < d2⊢ (Std.PRange.succMany? (d2.toNat - Day.mo.toNat.succ) Day.mo).bind Std.PRange.succ? = some d2mp.tud2:Daylt:Day.tu < d2⊢ (Std.PRange.succMany? (d2.toNat - Day.tu.toNat.succ) Day.tu).bind Std.PRange.succ? = some d2mp.wed2:Daylt:Day.we < d2⊢ (Std.PRange.succMany? (d2.toNat - Day.we.toNat.succ) Day.we).bind Std.PRange.succ? = some d2mp.thd2:Daylt:Day.th < d2⊢ (Std.PRange.succMany? (d2.toNat - Day.th.toNat.succ) Day.th).bind Std.PRange.succ? = some d2mp.frd2:Daylt:Day.fr < d2⊢ (Std.PRange.succMany? (d2.toNat - Day.fr.toNat.succ) Day.fr).bind Std.PRange.succ? = some d2mp.sad2:Daylt:Day.sa < d2⊢ (Std.PRange.succMany? (d2.toNat - Day.sa.toNat.succ) Day.sa).bind Std.PRange.succ? = some d2mp.sud2:Daylt:Day.su < d2⊢ (Std.PRange.succMany? (d2.toNat - Day.su.toNat.succ) Day.su).bind Std.PRange.succ? = some d2 cases d2mp.su.molt:Day.su < Day.mo⊢ (Std.PRange.succMany? (Day.mo.toNat - Day.su.toNat.succ) Day.su).bind Std.PRange.succ? = some Day.momp.su.tult:Day.su < Day.tu⊢ (Std.PRange.succMany? (Day.tu.toNat - Day.su.toNat.succ) Day.su).bind Std.PRange.succ? = some Day.tump.su.welt:Day.su < Day.we⊢ (Std.PRange.succMany? (Day.we.toNat - Day.su.toNat.succ) Day.su).bind Std.PRange.succ? = some Day.wemp.su.thlt:Day.su < Day.th⊢ (Std.PRange.succMany? (Day.th.toNat - Day.su.toNat.succ) Day.su).bind Std.PRange.succ? = some Day.thmp.su.frlt:Day.su < Day.fr⊢ (Std.PRange.succMany? (Day.fr.toNat - Day.su.toNat.succ) Day.su).bind Std.PRange.succ? = some Day.frmp.su.salt:Day.su < Day.sa⊢ (Std.PRange.succMany? (Day.sa.toNat - Day.su.toNat.succ) Day.su).bind Std.PRange.succ? = some Day.samp.su.sult:Day.su < Day.su⊢ (Std.PRange.succMany? (Day.su.toNat - Day.su.toNat.succ) Day.su).bind Std.PRange.succ? = some Day.su <;>mp.mo.molt:Day.mo < Day.mo⊢ (Std.PRange.succMany? (Day.mo.toNat - Day.mo.toNat.succ) Day.mo).bind Std.PRange.succ? = some Day.momp.mo.tult:Day.mo < Day.tu⊢ (Std.PRange.succMany? (Day.tu.toNat - Day.mo.toNat.succ) Day.mo).bind Std.PRange.succ? = some Day.tump.mo.welt:Day.mo < Day.we⊢ (Std.PRange.succMany? (Day.we.toNat - Day.mo.toNat.succ) Day.mo).bind Std.PRange.succ? = some Day.wemp.mo.thlt:Day.mo < Day.th⊢ (Std.PRange.succMany? (Day.th.toNat - Day.mo.toNat.succ) Day.mo).bind Std.PRange.succ? = some Day.thmp.mo.frlt:Day.mo < Day.fr⊢ (Std.PRange.succMany? (Day.fr.toNat - Day.mo.toNat.succ) Day.mo).bind Std.PRange.succ? = some Day.frmp.mo.salt:Day.mo < Day.sa⊢ (Std.PRange.succMany? (Day.sa.toNat - Day.mo.toNat.succ) Day.mo).bind Std.PRange.succ? = some Day.samp.mo.sult:Day.mo < Day.su⊢ (Std.PRange.succMany? (Day.su.toNat - Day.mo.toNat.succ) Day.mo).bind Std.PRange.succ? = some Day.sump.tu.molt:Day.tu < Day.mo⊢ (Std.PRange.succMany? (Day.mo.toNat - Day.tu.toNat.succ) Day.tu).bind Std.PRange.succ? = some Day.momp.tu.tult:Day.tu < Day.tu⊢ (Std.PRange.succMany? (Day.tu.toNat - Day.tu.toNat.succ) Day.tu).bind Std.PRange.succ? = some Day.tump.tu.welt:Day.tu < Day.we⊢ (Std.PRange.succMany? (Day.we.toNat - Day.tu.toNat.succ) Day.tu).bind Std.PRange.succ? = some Day.wemp.tu.thlt:Day.tu < Day.th⊢ (Std.PRange.succMany? (Day.th.toNat - Day.tu.toNat.succ) Day.tu).bind Std.PRange.succ? = some Day.thmp.tu.frlt:Day.tu < Day.fr⊢ (Std.PRange.succMany? (Day.fr.toNat - Day.tu.toNat.succ) Day.tu).bind Std.PRange.succ? = some Day.frmp.tu.salt:Day.tu < Day.sa⊢ (Std.PRange.succMany? (Day.sa.toNat - Day.tu.toNat.succ) Day.tu).bind Std.PRange.succ? = some Day.samp.tu.sult:Day.tu < Day.su⊢ (Std.PRange.succMany? (Day.su.toNat - Day.tu.toNat.succ) Day.tu).bind Std.PRange.succ? = some Day.sump.we.molt:Day.we < Day.mo⊢ (Std.PRange.succMany? (Day.mo.toNat - Day.we.toNat.succ) Day.we).bind Std.PRange.succ? = some Day.momp.we.tult:Day.we < Day.tu⊢ (Std.PRange.succMany? (Day.tu.toNat - Day.we.toNat.succ) Day.we).bind Std.PRange.succ? = some Day.tump.we.welt:Day.we < Day.we⊢ (Std.PRange.succMany? (Day.we.toNat - Day.we.toNat.succ) Day.we).bind Std.PRange.succ? = some Day.wemp.we.thlt:Day.we < Day.th⊢ (Std.PRange.succMany? (Day.th.toNat - Day.we.toNat.succ) Day.we).bind Std.PRange.succ? = some Day.thmp.we.frlt:Day.we < Day.fr⊢ (Std.PRange.succMany? (Day.fr.toNat - Day.we.toNat.succ) Day.we).bind Std.PRange.succ? = some Day.frmp.we.salt:Day.we < Day.sa⊢ (Std.PRange.succMany? (Day.sa.toNat - Day.we.toNat.succ) Day.we).bind Std.PRange.succ? = some Day.samp.we.sult:Day.we < Day.su⊢ (Std.PRange.succMany? (Day.su.toNat - Day.we.toNat.succ) Day.we).bind Std.PRange.succ? = some Day.sump.th.molt:Day.th < Day.mo⊢ (Std.PRange.succMany? (Day.mo.toNat - Day.th.toNat.succ) Day.th).bind Std.PRange.succ? = some Day.momp.th.tult:Day.th < Day.tu⊢ (Std.PRange.succMany? (Day.tu.toNat - Day.th.toNat.succ) Day.th).bind Std.PRange.succ? = some Day.tump.th.welt:Day.th < Day.we⊢ (Std.PRange.succMany? (Day.we.toNat - Day.th.toNat.succ) Day.th).bind Std.PRange.succ? = some Day.wemp.th.thlt:Day.th < Day.th⊢ (Std.PRange.succMany? (Day.th.toNat - Day.th.toNat.succ) Day.th).bind Std.PRange.succ? = some Day.thmp.th.frlt:Day.th < Day.fr⊢ (Std.PRange.succMany? (Day.fr.toNat - Day.th.toNat.succ) Day.th).bind Std.PRange.succ? = some Day.frmp.th.salt:Day.th < Day.sa⊢ (Std.PRange.succMany? (Day.sa.toNat - Day.th.toNat.succ) Day.th).bind Std.PRange.succ? = some Day.samp.th.sult:Day.th < Day.su⊢ (Std.PRange.succMany? (Day.su.toNat - Day.th.toNat.succ) Day.th).bind Std.PRange.succ? = some Day.sump.fr.molt:Day.fr < Day.mo⊢ (Std.PRange.succMany? (Day.mo.toNat - Day.fr.toNat.succ) Day.fr).bind Std.PRange.succ? = some Day.momp.fr.tult:Day.fr < Day.tu⊢ (Std.PRange.succMany? (Day.tu.toNat - Day.fr.toNat.succ) Day.fr).bind Std.PRange.succ? = some Day.tump.fr.welt:Day.fr < Day.we⊢ (Std.PRange.succMany? (Day.we.toNat - Day.fr.toNat.succ) Day.fr).bind Std.PRange.succ? = some Day.wemp.fr.thlt:Day.fr < Day.th⊢ (Std.PRange.succMany? (Day.th.toNat - Day.fr.toNat.succ) Day.fr).bind Std.PRange.succ? = some Day.thmp.fr.frlt:Day.fr < Day.fr⊢ (Std.PRange.succMany? (Day.fr.toNat - Day.fr.toNat.succ) Day.fr).bind Std.PRange.succ? = some Day.frmp.fr.salt:Day.fr < Day.sa⊢ (Std.PRange.succMany? (Day.sa.toNat - Day.fr.toNat.succ) Day.fr).bind Std.PRange.succ? = some Day.samp.fr.sult:Day.fr < Day.su⊢ (Std.PRange.succMany? (Day.su.toNat - Day.fr.toNat.succ) Day.fr).bind Std.PRange.succ? = some Day.sump.sa.molt:Day.sa < Day.mo⊢ (Std.PRange.succMany? (Day.mo.toNat - Day.sa.toNat.succ) Day.sa).bind Std.PRange.succ? = some Day.momp.sa.tult:Day.sa < Day.tu⊢ (Std.PRange.succMany? (Day.tu.toNat - Day.sa.toNat.succ) Day.sa).bind Std.PRange.succ? = some Day.tump.sa.welt:Day.sa < Day.we⊢ (Std.PRange.succMany? (Day.we.toNat - Day.sa.toNat.succ) Day.sa).bind Std.PRange.succ? = some Day.wemp.sa.thlt:Day.sa < Day.th⊢ (Std.PRange.succMany? (Day.th.toNat - Day.sa.toNat.succ) Day.sa).bind Std.PRange.succ? = some Day.thmp.sa.frlt:Day.sa < Day.fr⊢ (Std.PRange.succMany? (Day.fr.toNat - Day.sa.toNat.succ) Day.sa).bind Std.PRange.succ? = some Day.frmp.sa.salt:Day.sa < Day.sa⊢ (Std.PRange.succMany? (Day.sa.toNat - Day.sa.toNat.succ) Day.sa).bind Std.PRange.succ? = some Day.samp.sa.sult:Day.sa < Day.su⊢ (Std.PRange.succMany? (Day.su.toNat - Day.sa.toNat.succ) Day.sa).bind Std.PRange.succ? = some Day.sump.su.molt:Day.su < Day.mo⊢ (Std.PRange.succMany? (Day.mo.toNat - Day.su.toNat.succ) Day.su).bind Std.PRange.succ? = some Day.momp.su.tult:Day.su < Day.tu⊢ (Std.PRange.succMany? (Day.tu.toNat - Day.su.toNat.succ) Day.su).bind Std.PRange.succ? = some Day.tump.su.welt:Day.su < Day.we⊢ (Std.PRange.succMany? (Day.we.toNat - Day.su.toNat.succ) Day.su).bind Std.PRange.succ? = some Day.wemp.su.thlt:Day.su < Day.th⊢ (Std.PRange.succMany? (Day.th.toNat - Day.su.toNat.succ) Day.su).bind Std.PRange.succ? = some Day.thmp.su.frlt:Day.su < Day.fr⊢ (Std.PRange.succMany? (Day.fr.toNat - Day.su.toNat.succ) Day.su).bind Std.PRange.succ? = some Day.frmp.su.salt:Day.su < Day.sa⊢ (Std.PRange.succMany? (Day.sa.toNat - Day.su.toNat.succ) Day.su).bind Std.PRange.succ? = some Day.samp.su.sult:Day.su < Day.su⊢ (Std.PRange.succMany? (Day.su.toNat - Day.su.toNat.succ) Day.su).bind Std.PRange.succ? = some Day.su
      simp_all [Day.toNat, Std.PRange.succ?, Day.succ?]mp.su.sult:Day.su < Day.su⊢ False <;>mp.mo.molt:Day.mo < Day.mo⊢ Falsemp.tu.molt:Day.tu < Day.mo⊢ Falsemp.tu.tult:Day.tu < Day.tu⊢ Falsemp.we.molt:Day.we < Day.mo⊢ Falsemp.we.tult:Day.we < Day.tu⊢ Falsemp.we.welt:Day.we < Day.we⊢ Falsemp.th.molt:Day.th < Day.mo⊢ Falsemp.th.tult:Day.th < Day.tu⊢ Falsemp.th.welt:Day.th < Day.we⊢ Falsemp.th.thlt:Day.th < Day.th⊢ Falsemp.fr.molt:Day.fr < Day.mo⊢ Falsemp.fr.tult:Day.fr < Day.tu⊢ Falsemp.fr.welt:Day.fr < Day.we⊢ Falsemp.fr.thlt:Day.fr < Day.th⊢ Falsemp.fr.frlt:Day.fr < Day.fr⊢ Falsemp.sa.molt:Day.sa < Day.mo⊢ Falsemp.sa.tult:Day.sa < Day.tu⊢ Falsemp.sa.welt:Day.sa < Day.we⊢ Falsemp.sa.thlt:Day.sa < Day.th⊢ Falsemp.sa.frlt:Day.sa < Day.fr⊢ Falsemp.sa.salt:Day.sa < Day.sa⊢ Falsemp.su.molt:Day.su < Day.mo⊢ Falsemp.su.tult:Day.su < Day.tu⊢ Falsemp.su.welt:Day.su < Day.we⊢ Falsemp.su.thlt:Day.su < Day.th⊢ Falsemp.su.frlt:Day.su < Day.fr⊢ Falsemp.su.salt:Day.su < Day.sa⊢ Falsemp.su.sult:Day.su < Day.su⊢ False
      contradictionAll goals completed! 🐙
    .mprd1:Dayd2:Day⊢ Std.PRange.UpwardEnumerable.LT d1 d2 → d1 < d2 intro ⟨steps, eq⟩mprd1:Dayd2:Daysteps:Nateq:Std.PRange.succMany? (steps + 1) d1 = some d2⊢ d1 < d2
      have := Day.succMany?_steps eqmprd1:Dayd2:Daysteps:Nateq:Std.PRange.succMany? (steps + 1) d1 = some d2this:if d1 ≤ d2 then steps + 1 = d2.toNat - d1.toNat else False⊢ d1 < d2
      cases d1mpr.mod2:Daysteps:Nateq:Std.PRange.succMany? (steps + 1) Day.mo = some d2this:if Day.mo ≤ d2 then steps + 1 = d2.toNat - Day.mo.toNat else False⊢ Day.mo < d2mpr.tud2:Daysteps:Nateq:Std.PRange.succMany? (steps + 1) Day.tu = some d2this:if Day.tu ≤ d2 then steps + 1 = d2.toNat - Day.tu.toNat else False⊢ Day.tu < d2mpr.wed2:Daysteps:Nateq:Std.PRange.succMany? (steps + 1) Day.we = some d2this:if Day.we ≤ d2 then steps + 1 = d2.toNat - Day.we.toNat else False⊢ Day.we < d2mpr.thd2:Daysteps:Nateq:Std.PRange.succMany? (steps + 1) Day.th = some d2this:if Day.th ≤ d2 then steps + 1 = d2.toNat - Day.th.toNat else False⊢ Day.th < d2mpr.frd2:Daysteps:Nateq:Std.PRange.succMany? (steps + 1) Day.fr = some d2this:if Day.fr ≤ d2 then steps + 1 = d2.toNat - Day.fr.toNat else False⊢ Day.fr < d2mpr.sad2:Daysteps:Nateq:Std.PRange.succMany? (steps + 1) Day.sa = some d2this:if Day.sa ≤ d2 then steps + 1 = d2.toNat - Day.sa.toNat else False⊢ Day.sa < d2mpr.sud2:Daysteps:Nateq:Std.PRange.succMany? (steps + 1) Day.su = some d2this:if Day.su ≤ d2 then steps + 1 = d2.toNat - Day.su.toNat else False⊢ Day.su < d2 <;>mpr.mod2:Daysteps:Nateq:Std.PRange.succMany? (steps + 1) Day.mo = some d2this:if Day.mo ≤ d2 then steps + 1 = d2.toNat - Day.mo.toNat else False⊢ Day.mo < d2mpr.tud2:Daysteps:Nateq:Std.PRange.succMany? (steps + 1) Day.tu = some d2this:if Day.tu ≤ d2 then steps + 1 = d2.toNat - Day.tu.toNat else False⊢ Day.tu < d2mpr.wed2:Daysteps:Nateq:Std.PRange.succMany? (steps + 1) Day.we = some d2this:if Day.we ≤ d2 then steps + 1 = d2.toNat - Day.we.toNat else False⊢ Day.we < d2mpr.thd2:Daysteps:Nateq:Std.PRange.succMany? (steps + 1) Day.th = some d2this:if Day.th ≤ d2 then steps + 1 = d2.toNat - Day.th.toNat else False⊢ Day.th < d2mpr.frd2:Daysteps:Nateq:Std.PRange.succMany? (steps + 1) Day.fr = some d2this:if Day.fr ≤ d2 then steps + 1 = d2.toNat - Day.fr.toNat else False⊢ Day.fr < d2mpr.sad2:Daysteps:Nateq:Std.PRange.succMany? (steps + 1) Day.sa = some d2this:if Day.sa ≤ d2 then steps + 1 = d2.toNat - Day.sa.toNat else False⊢ Day.sa < d2mpr.sud2:Daysteps:Nateq:Std.PRange.succMany? (steps + 1) Day.su = some d2this:if Day.su ≤ d2 then steps + 1 = d2.toNat - Day.su.toNat else False⊢ Day.su < d2 cases d2mpr.su.mosteps:Nateq:Std.PRange.succMany? (steps + 1) Day.su = some Day.mothis:if Day.su ≤ Day.mo then steps + 1 = Day.mo.toNat - Day.su.toNat else False⊢ Day.su < Day.mompr.su.tusteps:Nateq:Std.PRange.succMany? (steps + 1) Day.su = some Day.tuthis:if Day.su ≤ Day.tu then steps + 1 = Day.tu.toNat - Day.su.toNat else False⊢ Day.su < Day.tumpr.su.westeps:Nateq:Std.PRange.succMany? (steps + 1) Day.su = some Day.wethis:if Day.su ≤ Day.we then steps + 1 = Day.we.toNat - Day.su.toNat else False⊢ Day.su < Day.wempr.su.thsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.su = some Day.ththis:if Day.su ≤ Day.th then steps + 1 = Day.th.toNat - Day.su.toNat else False⊢ Day.su < Day.thmpr.su.frsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.su = some Day.frthis:if Day.su ≤ Day.fr then steps + 1 = Day.fr.toNat - Day.su.toNat else False⊢ Day.su < Day.frmpr.su.sasteps:Nateq:Std.PRange.succMany? (steps + 1) Day.su = some Day.sathis:if Day.su ≤ Day.sa then steps + 1 = Day.sa.toNat - Day.su.toNat else False⊢ Day.su < Day.sampr.su.susteps:Nateq:Std.PRange.succMany? (steps + 1) Day.su = some Day.suthis:if Day.su ≤ Day.su then steps + 1 = Day.su.toNat - Day.su.toNat else False⊢ Day.su < Day.su <;>mpr.mo.mosteps:Nateq:Std.PRange.succMany? (steps + 1) Day.mo = some Day.mothis:if Day.mo ≤ Day.mo then steps + 1 = Day.mo.toNat - Day.mo.toNat else False⊢ Day.mo < Day.mompr.mo.tusteps:Nateq:Std.PRange.succMany? (steps + 1) Day.mo = some Day.tuthis:if Day.mo ≤ Day.tu then steps + 1 = Day.tu.toNat - Day.mo.toNat else False⊢ Day.mo < Day.tumpr.mo.westeps:Nateq:Std.PRange.succMany? (steps + 1) Day.mo = some Day.wethis:if Day.mo ≤ Day.we then steps + 1 = Day.we.toNat - Day.mo.toNat else False⊢ Day.mo < Day.wempr.mo.thsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.mo = some Day.ththis:if Day.mo ≤ Day.th then steps + 1 = Day.th.toNat - Day.mo.toNat else False⊢ Day.mo < Day.thmpr.mo.frsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.mo = some Day.frthis:if Day.mo ≤ Day.fr then steps + 1 = Day.fr.toNat - Day.mo.toNat else False⊢ Day.mo < Day.frmpr.mo.sasteps:Nateq:Std.PRange.succMany? (steps + 1) Day.mo = some Day.sathis:if Day.mo ≤ Day.sa then steps + 1 = Day.sa.toNat - Day.mo.toNat else False⊢ Day.mo < Day.sampr.mo.susteps:Nateq:Std.PRange.succMany? (steps + 1) Day.mo = some Day.suthis:if Day.mo ≤ Day.su then steps + 1 = Day.su.toNat - Day.mo.toNat else False⊢ Day.mo < Day.sumpr.tu.mosteps:Nateq:Std.PRange.succMany? (steps + 1) Day.tu = some Day.mothis:if Day.tu ≤ Day.mo then steps + 1 = Day.mo.toNat - Day.tu.toNat else False⊢ Day.tu < Day.mompr.tu.tusteps:Nateq:Std.PRange.succMany? (steps + 1) Day.tu = some Day.tuthis:if Day.tu ≤ Day.tu then steps + 1 = Day.tu.toNat - Day.tu.toNat else False⊢ Day.tu < Day.tumpr.tu.westeps:Nateq:Std.PRange.succMany? (steps + 1) Day.tu = some Day.wethis:if Day.tu ≤ Day.we then steps + 1 = Day.we.toNat - Day.tu.toNat else False⊢ Day.tu < Day.wempr.tu.thsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.tu = some Day.ththis:if Day.tu ≤ Day.th then steps + 1 = Day.th.toNat - Day.tu.toNat else False⊢ Day.tu < Day.thmpr.tu.frsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.tu = some Day.frthis:if Day.tu ≤ Day.fr then steps + 1 = Day.fr.toNat - Day.tu.toNat else False⊢ Day.tu < Day.frmpr.tu.sasteps:Nateq:Std.PRange.succMany? (steps + 1) Day.tu = some Day.sathis:if Day.tu ≤ Day.sa then steps + 1 = Day.sa.toNat - Day.tu.toNat else False⊢ Day.tu < Day.sampr.tu.susteps:Nateq:Std.PRange.succMany? (steps + 1) Day.tu = some Day.suthis:if Day.tu ≤ Day.su then steps + 1 = Day.su.toNat - Day.tu.toNat else False⊢ Day.tu < Day.sumpr.we.mosteps:Nateq:Std.PRange.succMany? (steps + 1) Day.we = some Day.mothis:if Day.we ≤ Day.mo then steps + 1 = Day.mo.toNat - Day.we.toNat else False⊢ Day.we < Day.mompr.we.tusteps:Nateq:Std.PRange.succMany? (steps + 1) Day.we = some Day.tuthis:if Day.we ≤ Day.tu then steps + 1 = Day.tu.toNat - Day.we.toNat else False⊢ Day.we < Day.tumpr.we.westeps:Nateq:Std.PRange.succMany? (steps + 1) Day.we = some Day.wethis:if Day.we ≤ Day.we then steps + 1 = Day.we.toNat - Day.we.toNat else False⊢ Day.we < Day.wempr.we.thsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.we = some Day.ththis:if Day.we ≤ Day.th then steps + 1 = Day.th.toNat - Day.we.toNat else False⊢ Day.we < Day.thmpr.we.frsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.we = some Day.frthis:if Day.we ≤ Day.fr then steps + 1 = Day.fr.toNat - Day.we.toNat else False⊢ Day.we < Day.frmpr.we.sasteps:Nateq:Std.PRange.succMany? (steps + 1) Day.we = some Day.sathis:if Day.we ≤ Day.sa then steps + 1 = Day.sa.toNat - Day.we.toNat else False⊢ Day.we < Day.sampr.we.susteps:Nateq:Std.PRange.succMany? (steps + 1) Day.we = some Day.suthis:if Day.we ≤ Day.su then steps + 1 = Day.su.toNat - Day.we.toNat else False⊢ Day.we < Day.sumpr.th.mosteps:Nateq:Std.PRange.succMany? (steps + 1) Day.th = some Day.mothis:if Day.th ≤ Day.mo then steps + 1 = Day.mo.toNat - Day.th.toNat else False⊢ Day.th < Day.mompr.th.tusteps:Nateq:Std.PRange.succMany? (steps + 1) Day.th = some Day.tuthis:if Day.th ≤ Day.tu then steps + 1 = Day.tu.toNat - Day.th.toNat else False⊢ Day.th < Day.tumpr.th.westeps:Nateq:Std.PRange.succMany? (steps + 1) Day.th = some Day.wethis:if Day.th ≤ Day.we then steps + 1 = Day.we.toNat - Day.th.toNat else False⊢ Day.th < Day.wempr.th.thsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.th = some Day.ththis:if Day.th ≤ Day.th then steps + 1 = Day.th.toNat - Day.th.toNat else False⊢ Day.th < Day.thmpr.th.frsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.th = some Day.frthis:if Day.th ≤ Day.fr then steps + 1 = Day.fr.toNat - Day.th.toNat else False⊢ Day.th < Day.frmpr.th.sasteps:Nateq:Std.PRange.succMany? (steps + 1) Day.th = some Day.sathis:if Day.th ≤ Day.sa then steps + 1 = Day.sa.toNat - Day.th.toNat else False⊢ Day.th < Day.sampr.th.susteps:Nateq:Std.PRange.succMany? (steps + 1) Day.th = some Day.suthis:if Day.th ≤ Day.su then steps + 1 = Day.su.toNat - Day.th.toNat else False⊢ Day.th < Day.sumpr.fr.mosteps:Nateq:Std.PRange.succMany? (steps + 1) Day.fr = some Day.mothis:if Day.fr ≤ Day.mo then steps + 1 = Day.mo.toNat - Day.fr.toNat else False⊢ Day.fr < Day.mompr.fr.tusteps:Nateq:Std.PRange.succMany? (steps + 1) Day.fr = some Day.tuthis:if Day.fr ≤ Day.tu then steps + 1 = Day.tu.toNat - Day.fr.toNat else False⊢ Day.fr < Day.tumpr.fr.westeps:Nateq:Std.PRange.succMany? (steps + 1) Day.fr = some Day.wethis:if Day.fr ≤ Day.we then steps + 1 = Day.we.toNat - Day.fr.toNat else False⊢ Day.fr < Day.wempr.fr.thsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.fr = some Day.ththis:if Day.fr ≤ Day.th then steps + 1 = Day.th.toNat - Day.fr.toNat else False⊢ Day.fr < Day.thmpr.fr.frsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.fr = some Day.frthis:if Day.fr ≤ Day.fr then steps + 1 = Day.fr.toNat - Day.fr.toNat else False⊢ Day.fr < Day.frmpr.fr.sasteps:Nateq:Std.PRange.succMany? (steps + 1) Day.fr = some Day.sathis:if Day.fr ≤ Day.sa then steps + 1 = Day.sa.toNat - Day.fr.toNat else False⊢ Day.fr < Day.sampr.fr.susteps:Nateq:Std.PRange.succMany? (steps + 1) Day.fr = some Day.suthis:if Day.fr ≤ Day.su then steps + 1 = Day.su.toNat - Day.fr.toNat else False⊢ Day.fr < Day.sumpr.sa.mosteps:Nateq:Std.PRange.succMany? (steps + 1) Day.sa = some Day.mothis:if Day.sa ≤ Day.mo then steps + 1 = Day.mo.toNat - Day.sa.toNat else False⊢ Day.sa < Day.mompr.sa.tusteps:Nateq:Std.PRange.succMany? (steps + 1) Day.sa = some Day.tuthis:if Day.sa ≤ Day.tu then steps + 1 = Day.tu.toNat - Day.sa.toNat else False⊢ Day.sa < Day.tumpr.sa.westeps:Nateq:Std.PRange.succMany? (steps + 1) Day.sa = some Day.wethis:if Day.sa ≤ Day.we then steps + 1 = Day.we.toNat - Day.sa.toNat else False⊢ Day.sa < Day.wempr.sa.thsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.sa = some Day.ththis:if Day.sa ≤ Day.th then steps + 1 = Day.th.toNat - Day.sa.toNat else False⊢ Day.sa < Day.thmpr.sa.frsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.sa = some Day.frthis:if Day.sa ≤ Day.fr then steps + 1 = Day.fr.toNat - Day.sa.toNat else False⊢ Day.sa < Day.frmpr.sa.sasteps:Nateq:Std.PRange.succMany? (steps + 1) Day.sa = some Day.sathis:if Day.sa ≤ Day.sa then steps + 1 = Day.sa.toNat - Day.sa.toNat else False⊢ Day.sa < Day.sampr.sa.susteps:Nateq:Std.PRange.succMany? (steps + 1) Day.sa = some Day.suthis:if Day.sa ≤ Day.su then steps + 1 = Day.su.toNat - Day.sa.toNat else False⊢ Day.sa < Day.sumpr.su.mosteps:Nateq:Std.PRange.succMany? (steps + 1) Day.su = some Day.mothis:if Day.su ≤ Day.mo then steps + 1 = Day.mo.toNat - Day.su.toNat else False⊢ Day.su < Day.mompr.su.tusteps:Nateq:Std.PRange.succMany? (steps + 1) Day.su = some Day.tuthis:if Day.su ≤ Day.tu then steps + 1 = Day.tu.toNat - Day.su.toNat else False⊢ Day.su < Day.tumpr.su.westeps:Nateq:Std.PRange.succMany? (steps + 1) Day.su = some Day.wethis:if Day.su ≤ Day.we then steps + 1 = Day.we.toNat - Day.su.toNat else False⊢ Day.su < Day.wempr.su.thsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.su = some Day.ththis:if Day.su ≤ Day.th then steps + 1 = Day.th.toNat - Day.su.toNat else False⊢ Day.su < Day.thmpr.su.frsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.su = some Day.frthis:if Day.su ≤ Day.fr then steps + 1 = Day.fr.toNat - Day.su.toNat else False⊢ Day.su < Day.frmpr.su.sasteps:Nateq:Std.PRange.succMany? (steps + 1) Day.su = some Day.sathis:if Day.su ≤ Day.sa then steps + 1 = Day.sa.toNat - Day.su.toNat else False⊢ Day.su < Day.sampr.su.susteps:Nateq:Std.PRange.succMany? (steps + 1) Day.su = some Day.suthis:if Day.su ≤ Day.su then steps + 1 = Day.su.toNat - Day.su.toNat else False⊢ Day.su < Day.su
      simp only [`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` insteadif_false_right] at thismpr.su.susteps:Nateq:Std.PRange.succMany? (steps + 1) Day.su = some Day.suthis:Day.su ≤ Day.su ∧ steps + 1 = Day.su.toNat - Day.su.toNat⊢ Day.su < Day.su <;>mpr.mo.mosteps:Nateq:Std.PRange.succMany? (steps + 1) Day.mo = some Day.mothis:Day.mo ≤ Day.mo ∧ steps + 1 = Day.mo.toNat - Day.mo.toNat⊢ Day.mo < Day.mompr.mo.tusteps:Nateq:Std.PRange.succMany? (steps + 1) Day.mo = some Day.tuthis:Day.mo ≤ Day.tu ∧ steps + 1 = Day.tu.toNat - Day.mo.toNat⊢ Day.mo < Day.tumpr.mo.westeps:Nateq:Std.PRange.succMany? (steps + 1) Day.mo = some Day.wethis:Day.mo ≤ Day.we ∧ steps + 1 = Day.we.toNat - Day.mo.toNat⊢ Day.mo < Day.wempr.mo.thsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.mo = some Day.ththis:Day.mo ≤ Day.th ∧ steps + 1 = Day.th.toNat - Day.mo.toNat⊢ Day.mo < Day.thmpr.mo.frsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.mo = some Day.frthis:Day.mo ≤ Day.fr ∧ steps + 1 = Day.fr.toNat - Day.mo.toNat⊢ Day.mo < Day.frmpr.mo.sasteps:Nateq:Std.PRange.succMany? (steps + 1) Day.mo = some Day.sathis:Day.mo ≤ Day.sa ∧ steps + 1 = Day.sa.toNat - Day.mo.toNat⊢ Day.mo < Day.sampr.mo.susteps:Nateq:Std.PRange.succMany? (steps + 1) Day.mo = some Day.suthis:Day.mo ≤ Day.su ∧ steps + 1 = Day.su.toNat - Day.mo.toNat⊢ Day.mo < Day.sumpr.tu.mosteps:Nateq:Std.PRange.succMany? (steps + 1) Day.tu = some Day.mothis:Day.tu ≤ Day.mo ∧ steps + 1 = Day.mo.toNat - Day.tu.toNat⊢ Day.tu < Day.mompr.tu.tusteps:Nateq:Std.PRange.succMany? (steps + 1) Day.tu = some Day.tuthis:Day.tu ≤ Day.tu ∧ steps + 1 = Day.tu.toNat - Day.tu.toNat⊢ Day.tu < Day.tumpr.tu.westeps:Nateq:Std.PRange.succMany? (steps + 1) Day.tu = some Day.wethis:Day.tu ≤ Day.we ∧ steps + 1 = Day.we.toNat - Day.tu.toNat⊢ Day.tu < Day.wempr.tu.thsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.tu = some Day.ththis:Day.tu ≤ Day.th ∧ steps + 1 = Day.th.toNat - Day.tu.toNat⊢ Day.tu < Day.thmpr.tu.frsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.tu = some Day.frthis:Day.tu ≤ Day.fr ∧ steps + 1 = Day.fr.toNat - Day.tu.toNat⊢ Day.tu < Day.frmpr.tu.sasteps:Nateq:Std.PRange.succMany? (steps + 1) Day.tu = some Day.sathis:Day.tu ≤ Day.sa ∧ steps + 1 = Day.sa.toNat - Day.tu.toNat⊢ Day.tu < Day.sampr.tu.susteps:Nateq:Std.PRange.succMany? (steps + 1) Day.tu = some Day.suthis:Day.tu ≤ Day.su ∧ steps + 1 = Day.su.toNat - Day.tu.toNat⊢ Day.tu < Day.sumpr.we.mosteps:Nateq:Std.PRange.succMany? (steps + 1) Day.we = some Day.mothis:Day.we ≤ Day.mo ∧ steps + 1 = Day.mo.toNat - Day.we.toNat⊢ Day.we < Day.mompr.we.tusteps:Nateq:Std.PRange.succMany? (steps + 1) Day.we = some Day.tuthis:Day.we ≤ Day.tu ∧ steps + 1 = Day.tu.toNat - Day.we.toNat⊢ Day.we < Day.tumpr.we.westeps:Nateq:Std.PRange.succMany? (steps + 1) Day.we = some Day.wethis:Day.we ≤ Day.we ∧ steps + 1 = Day.we.toNat - Day.we.toNat⊢ Day.we < Day.wempr.we.thsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.we = some Day.ththis:Day.we ≤ Day.th ∧ steps + 1 = Day.th.toNat - Day.we.toNat⊢ Day.we < Day.thmpr.we.frsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.we = some Day.frthis:Day.we ≤ Day.fr ∧ steps + 1 = Day.fr.toNat - Day.we.toNat⊢ Day.we < Day.frmpr.we.sasteps:Nateq:Std.PRange.succMany? (steps + 1) Day.we = some Day.sathis:Day.we ≤ Day.sa ∧ steps + 1 = Day.sa.toNat - Day.we.toNat⊢ Day.we < Day.sampr.we.susteps:Nateq:Std.PRange.succMany? (steps + 1) Day.we = some Day.suthis:Day.we ≤ Day.su ∧ steps + 1 = Day.su.toNat - Day.we.toNat⊢ Day.we < Day.sumpr.th.mosteps:Nateq:Std.PRange.succMany? (steps + 1) Day.th = some Day.mothis:Day.th ≤ Day.mo ∧ steps + 1 = Day.mo.toNat - Day.th.toNat⊢ Day.th < Day.mompr.th.tusteps:Nateq:Std.PRange.succMany? (steps + 1) Day.th = some Day.tuthis:Day.th ≤ Day.tu ∧ steps + 1 = Day.tu.toNat - Day.th.toNat⊢ Day.th < Day.tumpr.th.westeps:Nateq:Std.PRange.succMany? (steps + 1) Day.th = some Day.wethis:Day.th ≤ Day.we ∧ steps + 1 = Day.we.toNat - Day.th.toNat⊢ Day.th < Day.wempr.th.thsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.th = some Day.ththis:Day.th ≤ Day.th ∧ steps + 1 = Day.th.toNat - Day.th.toNat⊢ Day.th < Day.thmpr.th.frsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.th = some Day.frthis:Day.th ≤ Day.fr ∧ steps + 1 = Day.fr.toNat - Day.th.toNat⊢ Day.th < Day.frmpr.th.sasteps:Nateq:Std.PRange.succMany? (steps + 1) Day.th = some Day.sathis:Day.th ≤ Day.sa ∧ steps + 1 = Day.sa.toNat - Day.th.toNat⊢ Day.th < Day.sampr.th.susteps:Nateq:Std.PRange.succMany? (steps + 1) Day.th = some Day.suthis:Day.th ≤ Day.su ∧ steps + 1 = Day.su.toNat - Day.th.toNat⊢ Day.th < Day.sumpr.fr.mosteps:Nateq:Std.PRange.succMany? (steps + 1) Day.fr = some Day.mothis:Day.fr ≤ Day.mo ∧ steps + 1 = Day.mo.toNat - Day.fr.toNat⊢ Day.fr < Day.mompr.fr.tusteps:Nateq:Std.PRange.succMany? (steps + 1) Day.fr = some Day.tuthis:Day.fr ≤ Day.tu ∧ steps + 1 = Day.tu.toNat - Day.fr.toNat⊢ Day.fr < Day.tumpr.fr.westeps:Nateq:Std.PRange.succMany? (steps + 1) Day.fr = some Day.wethis:Day.fr ≤ Day.we ∧ steps + 1 = Day.we.toNat - Day.fr.toNat⊢ Day.fr < Day.wempr.fr.thsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.fr = some Day.ththis:Day.fr ≤ Day.th ∧ steps + 1 = Day.th.toNat - Day.fr.toNat⊢ Day.fr < Day.thmpr.fr.frsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.fr = some Day.frthis:Day.fr ≤ Day.fr ∧ steps + 1 = Day.fr.toNat - Day.fr.toNat⊢ Day.fr < Day.frmpr.fr.sasteps:Nateq:Std.PRange.succMany? (steps + 1) Day.fr = some Day.sathis:Day.fr ≤ Day.sa ∧ steps + 1 = Day.sa.toNat - Day.fr.toNat⊢ Day.fr < Day.sampr.fr.susteps:Nateq:Std.PRange.succMany? (steps + 1) Day.fr = some Day.suthis:Day.fr ≤ Day.su ∧ steps + 1 = Day.su.toNat - Day.fr.toNat⊢ Day.fr < Day.sumpr.sa.mosteps:Nateq:Std.PRange.succMany? (steps + 1) Day.sa = some Day.mothis:Day.sa ≤ Day.mo ∧ steps + 1 = Day.mo.toNat - Day.sa.toNat⊢ Day.sa < Day.mompr.sa.tusteps:Nateq:Std.PRange.succMany? (steps + 1) Day.sa = some Day.tuthis:Day.sa ≤ Day.tu ∧ steps + 1 = Day.tu.toNat - Day.sa.toNat⊢ Day.sa < Day.tumpr.sa.westeps:Nateq:Std.PRange.succMany? (steps + 1) Day.sa = some Day.wethis:Day.sa ≤ Day.we ∧ steps + 1 = Day.we.toNat - Day.sa.toNat⊢ Day.sa < Day.wempr.sa.thsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.sa = some Day.ththis:Day.sa ≤ Day.th ∧ steps + 1 = Day.th.toNat - Day.sa.toNat⊢ Day.sa < Day.thmpr.sa.frsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.sa = some Day.frthis:Day.sa ≤ Day.fr ∧ steps + 1 = Day.fr.toNat - Day.sa.toNat⊢ Day.sa < Day.frmpr.sa.sasteps:Nateq:Std.PRange.succMany? (steps + 1) Day.sa = some Day.sathis:Day.sa ≤ Day.sa ∧ steps + 1 = Day.sa.toNat - Day.sa.toNat⊢ Day.sa < Day.sampr.sa.susteps:Nateq:Std.PRange.succMany? (steps + 1) Day.sa = some Day.suthis:Day.sa ≤ Day.su ∧ steps + 1 = Day.su.toNat - Day.sa.toNat⊢ Day.sa < Day.sumpr.su.mosteps:Nateq:Std.PRange.succMany? (steps + 1) Day.su = some Day.mothis:Day.su ≤ Day.mo ∧ steps + 1 = Day.mo.toNat - Day.su.toNat⊢ Day.su < Day.mompr.su.tusteps:Nateq:Std.PRange.succMany? (steps + 1) Day.su = some Day.tuthis:Day.su ≤ Day.tu ∧ steps + 1 = Day.tu.toNat - Day.su.toNat⊢ Day.su < Day.tumpr.su.westeps:Nateq:Std.PRange.succMany? (steps + 1) Day.su = some Day.wethis:Day.su ≤ Day.we ∧ steps + 1 = Day.we.toNat - Day.su.toNat⊢ Day.su < Day.wempr.su.thsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.su = some Day.ththis:Day.su ≤ Day.th ∧ steps + 1 = Day.th.toNat - Day.su.toNat⊢ Day.su < Day.thmpr.su.frsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.su = some Day.frthis:Day.su ≤ Day.fr ∧ steps + 1 = Day.fr.toNat - Day.su.toNat⊢ Day.su < Day.frmpr.su.sasteps:Nateq:Std.PRange.succMany? (steps + 1) Day.su = some Day.sathis:Day.su ≤ Day.sa ∧ steps + 1 = Day.sa.toNat - Day.su.toNat⊢ Day.su < Day.sampr.su.susteps:Nateq:Std.PRange.succMany? (steps + 1) Day.su = some Day.suthis:Day.su ≤ Day.su ∧ steps + 1 = Day.su.toNat - Day.su.toNat⊢ Day.su < Day.su
      cases thismpr.su.su.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.su = some Day.suleft✝:Day.su ≤ Day.suright✝:steps + 1 = Day.su.toNat - Day.su.toNat⊢ Day.su < Day.su <;>mpr.mo.mo.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.mo = some Day.moleft✝:Day.mo ≤ Day.moright✝:steps + 1 = Day.mo.toNat - Day.mo.toNat⊢ Day.mo < Day.mompr.mo.tu.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.mo = some Day.tuleft✝:Day.mo ≤ Day.turight✝:steps + 1 = Day.tu.toNat - Day.mo.toNat⊢ Day.mo < Day.tumpr.mo.we.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.mo = some Day.weleft✝:Day.mo ≤ Day.weright✝:steps + 1 = Day.we.toNat - Day.mo.toNat⊢ Day.mo < Day.wempr.mo.th.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.mo = some Day.thleft✝:Day.mo ≤ Day.thright✝:steps + 1 = Day.th.toNat - Day.mo.toNat⊢ Day.mo < Day.thmpr.mo.fr.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.mo = some Day.frleft✝:Day.mo ≤ Day.frright✝:steps + 1 = Day.fr.toNat - Day.mo.toNat⊢ Day.mo < Day.frmpr.mo.sa.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.mo = some Day.saleft✝:Day.mo ≤ Day.saright✝:steps + 1 = Day.sa.toNat - Day.mo.toNat⊢ Day.mo < Day.sampr.mo.su.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.mo = some Day.suleft✝:Day.mo ≤ Day.suright✝:steps + 1 = Day.su.toNat - Day.mo.toNat⊢ Day.mo < Day.sumpr.tu.mo.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.tu = some Day.moleft✝:Day.tu ≤ Day.moright✝:steps + 1 = Day.mo.toNat - Day.tu.toNat⊢ Day.tu < Day.mompr.tu.tu.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.tu = some Day.tuleft✝:Day.tu ≤ Day.turight✝:steps + 1 = Day.tu.toNat - Day.tu.toNat⊢ Day.tu < Day.tumpr.tu.we.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.tu = some Day.weleft✝:Day.tu ≤ Day.weright✝:steps + 1 = Day.we.toNat - Day.tu.toNat⊢ Day.tu < Day.wempr.tu.th.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.tu = some Day.thleft✝:Day.tu ≤ Day.thright✝:steps + 1 = Day.th.toNat - Day.tu.toNat⊢ Day.tu < Day.thmpr.tu.fr.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.tu = some Day.frleft✝:Day.tu ≤ Day.frright✝:steps + 1 = Day.fr.toNat - Day.tu.toNat⊢ Day.tu < Day.frmpr.tu.sa.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.tu = some Day.saleft✝:Day.tu ≤ Day.saright✝:steps + 1 = Day.sa.toNat - Day.tu.toNat⊢ Day.tu < Day.sampr.tu.su.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.tu = some Day.suleft✝:Day.tu ≤ Day.suright✝:steps + 1 = Day.su.toNat - Day.tu.toNat⊢ Day.tu < Day.sumpr.we.mo.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.we = some Day.moleft✝:Day.we ≤ Day.moright✝:steps + 1 = Day.mo.toNat - Day.we.toNat⊢ Day.we < Day.mompr.we.tu.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.we = some Day.tuleft✝:Day.we ≤ Day.turight✝:steps + 1 = Day.tu.toNat - Day.we.toNat⊢ Day.we < Day.tumpr.we.we.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.we = some Day.weleft✝:Day.we ≤ Day.weright✝:steps + 1 = Day.we.toNat - Day.we.toNat⊢ Day.we < Day.wempr.we.th.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.we = some Day.thleft✝:Day.we ≤ Day.thright✝:steps + 1 = Day.th.toNat - Day.we.toNat⊢ Day.we < Day.thmpr.we.fr.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.we = some Day.frleft✝:Day.we ≤ Day.frright✝:steps + 1 = Day.fr.toNat - Day.we.toNat⊢ Day.we < Day.frmpr.we.sa.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.we = some Day.saleft✝:Day.we ≤ Day.saright✝:steps + 1 = Day.sa.toNat - Day.we.toNat⊢ Day.we < Day.sampr.we.su.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.we = some Day.suleft✝:Day.we ≤ Day.suright✝:steps + 1 = Day.su.toNat - Day.we.toNat⊢ Day.we < Day.sumpr.th.mo.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.th = some Day.moleft✝:Day.th ≤ Day.moright✝:steps + 1 = Day.mo.toNat - Day.th.toNat⊢ Day.th < Day.mompr.th.tu.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.th = some Day.tuleft✝:Day.th ≤ Day.turight✝:steps + 1 = Day.tu.toNat - Day.th.toNat⊢ Day.th < Day.tumpr.th.we.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.th = some Day.weleft✝:Day.th ≤ Day.weright✝:steps + 1 = Day.we.toNat - Day.th.toNat⊢ Day.th < Day.wempr.th.th.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.th = some Day.thleft✝:Day.th ≤ Day.thright✝:steps + 1 = Day.th.toNat - Day.th.toNat⊢ Day.th < Day.thmpr.th.fr.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.th = some Day.frleft✝:Day.th ≤ Day.frright✝:steps + 1 = Day.fr.toNat - Day.th.toNat⊢ Day.th < Day.frmpr.th.sa.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.th = some Day.saleft✝:Day.th ≤ Day.saright✝:steps + 1 = Day.sa.toNat - Day.th.toNat⊢ Day.th < Day.sampr.th.su.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.th = some Day.suleft✝:Day.th ≤ Day.suright✝:steps + 1 = Day.su.toNat - Day.th.toNat⊢ Day.th < Day.sumpr.fr.mo.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.fr = some Day.moleft✝:Day.fr ≤ Day.moright✝:steps + 1 = Day.mo.toNat - Day.fr.toNat⊢ Day.fr < Day.mompr.fr.tu.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.fr = some Day.tuleft✝:Day.fr ≤ Day.turight✝:steps + 1 = Day.tu.toNat - Day.fr.toNat⊢ Day.fr < Day.tumpr.fr.we.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.fr = some Day.weleft✝:Day.fr ≤ Day.weright✝:steps + 1 = Day.we.toNat - Day.fr.toNat⊢ Day.fr < Day.wempr.fr.th.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.fr = some Day.thleft✝:Day.fr ≤ Day.thright✝:steps + 1 = Day.th.toNat - Day.fr.toNat⊢ Day.fr < Day.thmpr.fr.fr.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.fr = some Day.frleft✝:Day.fr ≤ Day.frright✝:steps + 1 = Day.fr.toNat - Day.fr.toNat⊢ Day.fr < Day.frmpr.fr.sa.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.fr = some Day.saleft✝:Day.fr ≤ Day.saright✝:steps + 1 = Day.sa.toNat - Day.fr.toNat⊢ Day.fr < Day.sampr.fr.su.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.fr = some Day.suleft✝:Day.fr ≤ Day.suright✝:steps + 1 = Day.su.toNat - Day.fr.toNat⊢ Day.fr < Day.sumpr.sa.mo.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.sa = some Day.moleft✝:Day.sa ≤ Day.moright✝:steps + 1 = Day.mo.toNat - Day.sa.toNat⊢ Day.sa < Day.mompr.sa.tu.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.sa = some Day.tuleft✝:Day.sa ≤ Day.turight✝:steps + 1 = Day.tu.toNat - Day.sa.toNat⊢ Day.sa < Day.tumpr.sa.we.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.sa = some Day.weleft✝:Day.sa ≤ Day.weright✝:steps + 1 = Day.we.toNat - Day.sa.toNat⊢ Day.sa < Day.wempr.sa.th.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.sa = some Day.thleft✝:Day.sa ≤ Day.thright✝:steps + 1 = Day.th.toNat - Day.sa.toNat⊢ Day.sa < Day.thmpr.sa.fr.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.sa = some Day.frleft✝:Day.sa ≤ Day.frright✝:steps + 1 = Day.fr.toNat - Day.sa.toNat⊢ Day.sa < Day.frmpr.sa.sa.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.sa = some Day.saleft✝:Day.sa ≤ Day.saright✝:steps + 1 = Day.sa.toNat - Day.sa.toNat⊢ Day.sa < Day.sampr.sa.su.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.sa = some Day.suleft✝:Day.sa ≤ Day.suright✝:steps + 1 = Day.su.toNat - Day.sa.toNat⊢ Day.sa < Day.sumpr.su.mo.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.su = some Day.moleft✝:Day.su ≤ Day.moright✝:steps + 1 = Day.mo.toNat - Day.su.toNat⊢ Day.su < Day.mompr.su.tu.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.su = some Day.tuleft✝:Day.su ≤ Day.turight✝:steps + 1 = Day.tu.toNat - Day.su.toNat⊢ Day.su < Day.tumpr.su.we.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.su = some Day.weleft✝:Day.su ≤ Day.weright✝:steps + 1 = Day.we.toNat - Day.su.toNat⊢ Day.su < Day.wempr.su.th.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.su = some Day.thleft✝:Day.su ≤ Day.thright✝:steps + 1 = Day.th.toNat - Day.su.toNat⊢ Day.su < Day.thmpr.su.fr.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.su = some Day.frleft✝:Day.su ≤ Day.frright✝:steps + 1 = Day.fr.toNat - Day.su.toNat⊢ Day.su < Day.frmpr.su.sa.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.su = some Day.saleft✝:Day.su ≤ Day.saright✝:steps + 1 = Day.sa.toNat - Day.su.toNat⊢ Day.su < Day.sampr.su.su.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.su = some Day.suleft✝:Day.su ≤ Day.suright✝:steps + 1 = Day.su.toNat - Day.su.toNat⊢ Day.su < Day.su first | decidempr.su.su.introsteps:Nateq:Std.PRange.succMany? (steps + 1) Day.su = some Day.suleft✝:Day.su ≤ Day.suright✝:steps + 1 = Day.su.toNat - Day.su.toNat⊢ Day.su < Day.su | contradictionAll goals completed! 🐙

instance : Std.PRange.LawfulUpwardEnumerableLE Day where
  le_iff d1 d2 := byd1:Dayd2:Day⊢ d1 ≤ d2 ↔ Std.PRange.UpwardEnumerable.LE d1 d2
    constructormpd1:Dayd2:Day⊢ d1 ≤ d2 → Std.PRange.UpwardEnumerable.LE d1 d2mprd1:Dayd2:Day⊢ Std.PRange.UpwardEnumerable.LE d1 d2 → d1 ≤ d2
    .mpd1:Dayd2:Day⊢ d1 ≤ d2 → Std.PRange.UpwardEnumerable.LE d1 d2 intro lempd1:Dayd2:Dayle:d1 ≤ d2⊢ Std.PRange.UpwardEnumerable.LE d1 d2
      simp only [Std.PRange.UpwardEnumerable.LE]mpd1:Dayd2:Dayle:d1 ≤ d2⊢ ∃ n, Std.PRange.succMany? n d1 = some d2
      exists d2.toNat - d1.toNatmpd1:Dayd2:Dayle:d1 ≤ d2⊢ Std.PRange.succMany? (d2.toNat - d1.toNat) d1 = some d2
      cases d1mp.mod2:Dayle:Day.mo ≤ d2⊢ Std.PRange.succMany? (d2.toNat - Day.mo.toNat) Day.mo = some d2mp.tud2:Dayle:Day.tu ≤ d2⊢ Std.PRange.succMany? (d2.toNat - Day.tu.toNat) Day.tu = some d2mp.wed2:Dayle:Day.we ≤ d2⊢ Std.PRange.succMany? (d2.toNat - Day.we.toNat) Day.we = some d2mp.thd2:Dayle:Day.th ≤ d2⊢ Std.PRange.succMany? (d2.toNat - Day.th.toNat) Day.th = some d2mp.frd2:Dayle:Day.fr ≤ d2⊢ Std.PRange.succMany? (d2.toNat - Day.fr.toNat) Day.fr = some d2mp.sad2:Dayle:Day.sa ≤ d2⊢ Std.PRange.succMany? (d2.toNat - Day.sa.toNat) Day.sa = some d2mp.sud2:Dayle:Day.su ≤ d2⊢ Std.PRange.succMany? (d2.toNat - Day.su.toNat) Day.su = some d2 <;>mp.mod2:Dayle:Day.mo ≤ d2⊢ Std.PRange.succMany? (d2.toNat - Day.mo.toNat) Day.mo = some d2mp.tud2:Dayle:Day.tu ≤ d2⊢ Std.PRange.succMany? (d2.toNat - Day.tu.toNat) Day.tu = some d2mp.wed2:Dayle:Day.we ≤ d2⊢ Std.PRange.succMany? (d2.toNat - Day.we.toNat) Day.we = some d2mp.thd2:Dayle:Day.th ≤ d2⊢ Std.PRange.succMany? (d2.toNat - Day.th.toNat) Day.th = some d2mp.frd2:Dayle:Day.fr ≤ d2⊢ Std.PRange.succMany? (d2.toNat - Day.fr.toNat) Day.fr = some d2mp.sad2:Dayle:Day.sa ≤ d2⊢ Std.PRange.succMany? (d2.toNat - Day.sa.toNat) Day.sa = some d2mp.sud2:Dayle:Day.su ≤ d2⊢ Std.PRange.succMany? (d2.toNat - Day.su.toNat) Day.su = some d2 cases d2mp.su.mole:Day.su ≤ Day.mo⊢ Std.PRange.succMany? (Day.mo.toNat - Day.su.toNat) Day.su = some Day.momp.su.tule:Day.su ≤ Day.tu⊢ Std.PRange.succMany? (Day.tu.toNat - Day.su.toNat) Day.su = some Day.tump.su.wele:Day.su ≤ Day.we⊢ Std.PRange.succMany? (Day.we.toNat - Day.su.toNat) Day.su = some Day.wemp.su.thle:Day.su ≤ Day.th⊢ Std.PRange.succMany? (Day.th.toNat - Day.su.toNat) Day.su = some Day.thmp.su.frle:Day.su ≤ Day.fr⊢ Std.PRange.succMany? (Day.fr.toNat - Day.su.toNat) Day.su = some Day.frmp.su.sale:Day.su ≤ Day.sa⊢ Std.PRange.succMany? (Day.sa.toNat - Day.su.toNat) Day.su = some Day.samp.su.sule:Day.su ≤ Day.su⊢ Std.PRange.succMany? (Day.su.toNat - Day.su.toNat) Day.su = some Day.su <;>mp.mo.mole:Day.mo ≤ Day.mo⊢ Std.PRange.succMany? (Day.mo.toNat - Day.mo.toNat) Day.mo = some Day.momp.mo.tule:Day.mo ≤ Day.tu⊢ Std.PRange.succMany? (Day.tu.toNat - Day.mo.toNat) Day.mo = some Day.tump.mo.wele:Day.mo ≤ Day.we⊢ Std.PRange.succMany? (Day.we.toNat - Day.mo.toNat) Day.mo = some Day.wemp.mo.thle:Day.mo ≤ Day.th⊢ Std.PRange.succMany? (Day.th.toNat - Day.mo.toNat) Day.mo = some Day.thmp.mo.frle:Day.mo ≤ Day.fr⊢ Std.PRange.succMany? (Day.fr.toNat - Day.mo.toNat) Day.mo = some Day.frmp.mo.sale:Day.mo ≤ Day.sa⊢ Std.PRange.succMany? (Day.sa.toNat - Day.mo.toNat) Day.mo = some Day.samp.mo.sule:Day.mo ≤ Day.su⊢ Std.PRange.succMany? (Day.su.toNat - Day.mo.toNat) Day.mo = some Day.sump.tu.mole:Day.tu ≤ Day.mo⊢ Std.PRange.succMany? (Day.mo.toNat - Day.tu.toNat) Day.tu = some Day.momp.tu.tule:Day.tu ≤ Day.tu⊢ Std.PRange.succMany? (Day.tu.toNat - Day.tu.toNat) Day.tu = some Day.tump.tu.wele:Day.tu ≤ Day.we⊢ Std.PRange.succMany? (Day.we.toNat - Day.tu.toNat) Day.tu = some Day.wemp.tu.thle:Day.tu ≤ Day.th⊢ Std.PRange.succMany? (Day.th.toNat - Day.tu.toNat) Day.tu = some Day.thmp.tu.frle:Day.tu ≤ Day.fr⊢ Std.PRange.succMany? (Day.fr.toNat - Day.tu.toNat) Day.tu = some Day.frmp.tu.sale:Day.tu ≤ Day.sa⊢ Std.PRange.succMany? (Day.sa.toNat - Day.tu.toNat) Day.tu = some Day.samp.tu.sule:Day.tu ≤ Day.su⊢ Std.PRange.succMany? (Day.su.toNat - Day.tu.toNat) Day.tu = some Day.sump.we.mole:Day.we ≤ Day.mo⊢ Std.PRange.succMany? (Day.mo.toNat - Day.we.toNat) Day.we = some Day.momp.we.tule:Day.we ≤ Day.tu⊢ Std.PRange.succMany? (Day.tu.toNat - Day.we.toNat) Day.we = some Day.tump.we.wele:Day.we ≤ Day.we⊢ Std.PRange.succMany? (Day.we.toNat - Day.we.toNat) Day.we = some Day.wemp.we.thle:Day.we ≤ Day.th⊢ Std.PRange.succMany? (Day.th.toNat - Day.we.toNat) Day.we = some Day.thmp.we.frle:Day.we ≤ Day.fr⊢ Std.PRange.succMany? (Day.fr.toNat - Day.we.toNat) Day.we = some Day.frmp.we.sale:Day.we ≤ Day.sa⊢ Std.PRange.succMany? (Day.sa.toNat - Day.we.toNat) Day.we = some Day.samp.we.sule:Day.we ≤ Day.su⊢ Std.PRange.succMany? (Day.su.toNat - Day.we.toNat) Day.we = some Day.sump.th.mole:Day.th ≤ Day.mo⊢ Std.PRange.succMany? (Day.mo.toNat - Day.th.toNat) Day.th = some Day.momp.th.tule:Day.th ≤ Day.tu⊢ Std.PRange.succMany? (Day.tu.toNat - Day.th.toNat) Day.th = some Day.tump.th.wele:Day.th ≤ Day.we⊢ Std.PRange.succMany? (Day.we.toNat - Day.th.toNat) Day.th = some Day.wemp.th.thle:Day.th ≤ Day.th⊢ Std.PRange.succMany? (Day.th.toNat - Day.th.toNat) Day.th = some Day.thmp.th.frle:Day.th ≤ Day.fr⊢ Std.PRange.succMany? (Day.fr.toNat - Day.th.toNat) Day.th = some Day.frmp.th.sale:Day.th ≤ Day.sa⊢ Std.PRange.succMany? (Day.sa.toNat - Day.th.toNat) Day.th = some Day.samp.th.sule:Day.th ≤ Day.su⊢ Std.PRange.succMany? (Day.su.toNat - Day.th.toNat) Day.th = some Day.sump.fr.mole:Day.fr ≤ Day.mo⊢ Std.PRange.succMany? (Day.mo.toNat - Day.fr.toNat) Day.fr = some Day.momp.fr.tule:Day.fr ≤ Day.tu⊢ Std.PRange.succMany? (Day.tu.toNat - Day.fr.toNat) Day.fr = some Day.tump.fr.wele:Day.fr ≤ Day.we⊢ Std.PRange.succMany? (Day.we.toNat - Day.fr.toNat) Day.fr = some Day.wemp.fr.thle:Day.fr ≤ Day.th⊢ Std.PRange.succMany? (Day.th.toNat - Day.fr.toNat) Day.fr = some Day.thmp.fr.frle:Day.fr ≤ Day.fr⊢ Std.PRange.succMany? (Day.fr.toNat - Day.fr.toNat) Day.fr = some Day.frmp.fr.sale:Day.fr ≤ Day.sa⊢ Std.PRange.succMany? (Day.sa.toNat - Day.fr.toNat) Day.fr = some Day.samp.fr.sule:Day.fr ≤ Day.su⊢ Std.PRange.succMany? (Day.su.toNat - Day.fr.toNat) Day.fr = some Day.sump.sa.mole:Day.sa ≤ Day.mo⊢ Std.PRange.succMany? (Day.mo.toNat - Day.sa.toNat) Day.sa = some Day.momp.sa.tule:Day.sa ≤ Day.tu⊢ Std.PRange.succMany? (Day.tu.toNat - Day.sa.toNat) Day.sa = some Day.tump.sa.wele:Day.sa ≤ Day.we⊢ Std.PRange.succMany? (Day.we.toNat - Day.sa.toNat) Day.sa = some Day.wemp.sa.thle:Day.sa ≤ Day.th⊢ Std.PRange.succMany? (Day.th.toNat - Day.sa.toNat) Day.sa = some Day.thmp.sa.frle:Day.sa ≤ Day.fr⊢ Std.PRange.succMany? (Day.fr.toNat - Day.sa.toNat) Day.sa = some Day.frmp.sa.sale:Day.sa ≤ Day.sa⊢ Std.PRange.succMany? (Day.sa.toNat - Day.sa.toNat) Day.sa = some Day.samp.sa.sule:Day.sa ≤ Day.su⊢ Std.PRange.succMany? (Day.su.toNat - Day.sa.toNat) Day.sa = some Day.sump.su.mole:Day.su ≤ Day.mo⊢ Std.PRange.succMany? (Day.mo.toNat - Day.su.toNat) Day.su = some Day.momp.su.tule:Day.su ≤ Day.tu⊢ Std.PRange.succMany? (Day.tu.toNat - Day.su.toNat) Day.su = some Day.tump.su.wele:Day.su ≤ Day.we⊢ Std.PRange.succMany? (Day.we.toNat - Day.su.toNat) Day.su = some Day.wemp.su.thle:Day.su ≤ Day.th⊢ Std.PRange.succMany? (Day.th.toNat - Day.su.toNat) Day.su = some Day.thmp.su.frle:Day.su ≤ Day.fr⊢ Std.PRange.succMany? (Day.fr.toNat - Day.su.toNat) Day.su = some Day.frmp.su.sale:Day.su ≤ Day.sa⊢ Std.PRange.succMany? (Day.sa.toNat - Day.su.toNat) Day.su = some Day.samp.su.sule:Day.su ≤ Day.su⊢ Std.PRange.succMany? (Day.su.toNat - Day.su.toNat) Day.su = some Day.su
      simp_all [Day.toNat, Std.PRange.succ?, Day.succ?]All goals completed! 🐙 <;>mp.tu.mole:Day.tu ≤ Day.mo⊢ Falsemp.we.mole:Day.we ≤ Day.mo⊢ Falsemp.we.tule:Day.we ≤ Day.tu⊢ Falsemp.th.mole:Day.th ≤ Day.mo⊢ Falsemp.th.tule:Day.th ≤ Day.tu⊢ Falsemp.th.wele:Day.th ≤ Day.we⊢ Falsemp.fr.mole:Day.fr ≤ Day.mo⊢ Falsemp.fr.tule:Day.fr ≤ Day.tu⊢ Falsemp.fr.wele:Day.fr ≤ Day.we⊢ Falsemp.fr.thle:Day.fr ≤ Day.th⊢ Falsemp.sa.mole:Day.sa ≤ Day.mo⊢ Falsemp.sa.tule:Day.sa ≤ Day.tu⊢ Falsemp.sa.wele:Day.sa ≤ Day.we⊢ Falsemp.sa.thle:Day.sa ≤ Day.th⊢ Falsemp.sa.frle:Day.sa ≤ Day.fr⊢ Falsemp.su.mole:Day.su ≤ Day.mo⊢ Falsemp.su.tule:Day.su ≤ Day.tu⊢ Falsemp.su.wele:Day.su ≤ Day.we⊢ Falsemp.su.thle:Day.su ≤ Day.th⊢ Falsemp.su.frle:Day.su ≤ Day.fr⊢ Falsemp.su.sale:Day.su ≤ Day.sa⊢ False
      contradictionAll goals completed! 🐙
    .mprd1:Dayd2:Day⊢ Std.PRange.UpwardEnumerable.LE d1 d2 → d1 ≤ d2 intro ⟨steps, eq⟩mprd1:Dayd2:Daysteps:Nateq:Std.PRange.succMany? steps d1 = some d2⊢ d1 ≤ d2
      have := Day.succMany?_steps eqmprd1:Dayd2:Daysteps:Nateq:Std.PRange.succMany? steps d1 = some d2this:if d1 ≤ d2 then steps = d2.toNat - d1.toNat else False⊢ d1 ≤ d2
      cases d1mpr.mod2:Daysteps:Nateq:Std.PRange.succMany? steps Day.mo = some d2this:if Day.mo ≤ d2 then steps = d2.toNat - Day.mo.toNat else False⊢ Day.mo ≤ d2mpr.tud2:Daysteps:Nateq:Std.PRange.succMany? steps Day.tu = some d2this:if Day.tu ≤ d2 then steps = d2.toNat - Day.tu.toNat else False⊢ Day.tu ≤ d2mpr.wed2:Daysteps:Nateq:Std.PRange.succMany? steps Day.we = some d2this:if Day.we ≤ d2 then steps = d2.toNat - Day.we.toNat else False⊢ Day.we ≤ d2mpr.thd2:Daysteps:Nateq:Std.PRange.succMany? steps Day.th = some d2this:if Day.th ≤ d2 then steps = d2.toNat - Day.th.toNat else False⊢ Day.th ≤ d2mpr.frd2:Daysteps:Nateq:Std.PRange.succMany? steps Day.fr = some d2this:if Day.fr ≤ d2 then steps = d2.toNat - Day.fr.toNat else False⊢ Day.fr ≤ d2mpr.sad2:Daysteps:Nateq:Std.PRange.succMany? steps Day.sa = some d2this:if Day.sa ≤ d2 then steps = d2.toNat - Day.sa.toNat else False⊢ Day.sa ≤ d2mpr.sud2:Daysteps:Nateq:Std.PRange.succMany? steps Day.su = some d2this:if Day.su ≤ d2 then steps = d2.toNat - Day.su.toNat else False⊢ Day.su ≤ d2 <;>mpr.mod2:Daysteps:Nateq:Std.PRange.succMany? steps Day.mo = some d2this:if Day.mo ≤ d2 then steps = d2.toNat - Day.mo.toNat else False⊢ Day.mo ≤ d2mpr.tud2:Daysteps:Nateq:Std.PRange.succMany? steps Day.tu = some d2this:if Day.tu ≤ d2 then steps = d2.toNat - Day.tu.toNat else False⊢ Day.tu ≤ d2mpr.wed2:Daysteps:Nateq:Std.PRange.succMany? steps Day.we = some d2this:if Day.we ≤ d2 then steps = d2.toNat - Day.we.toNat else False⊢ Day.we ≤ d2mpr.thd2:Daysteps:Nateq:Std.PRange.succMany? steps Day.th = some d2this:if Day.th ≤ d2 then steps = d2.toNat - Day.th.toNat else False⊢ Day.th ≤ d2mpr.frd2:Daysteps:Nateq:Std.PRange.succMany? steps Day.fr = some d2this:if Day.fr ≤ d2 then steps = d2.toNat - Day.fr.toNat else False⊢ Day.fr ≤ d2mpr.sad2:Daysteps:Nateq:Std.PRange.succMany? steps Day.sa = some d2this:if Day.sa ≤ d2 then steps = d2.toNat - Day.sa.toNat else False⊢ Day.sa ≤ d2mpr.sud2:Daysteps:Nateq:Std.PRange.succMany? steps Day.su = some d2this:if Day.su ≤ d2 then steps = d2.toNat - Day.su.toNat else False⊢ Day.su ≤ d2 cases d2mpr.su.mosteps:Nateq:Std.PRange.succMany? steps Day.su = some Day.mothis:if Day.su ≤ Day.mo then steps = Day.mo.toNat - Day.su.toNat else False⊢ Day.su ≤ Day.mompr.su.tusteps:Nateq:Std.PRange.succMany? steps Day.su = some Day.tuthis:if Day.su ≤ Day.tu then steps = Day.tu.toNat - Day.su.toNat else False⊢ Day.su ≤ Day.tumpr.su.westeps:Nateq:Std.PRange.succMany? steps Day.su = some Day.wethis:if Day.su ≤ Day.we then steps = Day.we.toNat - Day.su.toNat else False⊢ Day.su ≤ Day.wempr.su.thsteps:Nateq:Std.PRange.succMany? steps Day.su = some Day.ththis:if Day.su ≤ Day.th then steps = Day.th.toNat - Day.su.toNat else False⊢ Day.su ≤ Day.thmpr.su.frsteps:Nateq:Std.PRange.succMany? steps Day.su = some Day.frthis:if Day.su ≤ Day.fr then steps = Day.fr.toNat - Day.su.toNat else False⊢ Day.su ≤ Day.frmpr.su.sasteps:Nateq:Std.PRange.succMany? steps Day.su = some Day.sathis:if Day.su ≤ Day.sa then steps = Day.sa.toNat - Day.su.toNat else False⊢ Day.su ≤ Day.sampr.su.susteps:Nateq:Std.PRange.succMany? steps Day.su = some Day.suthis:if Day.su ≤ Day.su then steps = Day.su.toNat - Day.su.toNat else False⊢ Day.su ≤ Day.su <;>mpr.mo.mosteps:Nateq:Std.PRange.succMany? steps Day.mo = some Day.mothis:if Day.mo ≤ Day.mo then steps = Day.mo.toNat - Day.mo.toNat else False⊢ Day.mo ≤ Day.mompr.mo.tusteps:Nateq:Std.PRange.succMany? steps Day.mo = some Day.tuthis:if Day.mo ≤ Day.tu then steps = Day.tu.toNat - Day.mo.toNat else False⊢ Day.mo ≤ Day.tumpr.mo.westeps:Nateq:Std.PRange.succMany? steps Day.mo = some Day.wethis:if Day.mo ≤ Day.we then steps = Day.we.toNat - Day.mo.toNat else False⊢ Day.mo ≤ Day.wempr.mo.thsteps:Nateq:Std.PRange.succMany? steps Day.mo = some Day.ththis:if Day.mo ≤ Day.th then steps = Day.th.toNat - Day.mo.toNat else False⊢ Day.mo ≤ Day.thmpr.mo.frsteps:Nateq:Std.PRange.succMany? steps Day.mo = some Day.frthis:if Day.mo ≤ Day.fr then steps = Day.fr.toNat - Day.mo.toNat else False⊢ Day.mo ≤ Day.frmpr.mo.sasteps:Nateq:Std.PRange.succMany? steps Day.mo = some Day.sathis:if Day.mo ≤ Day.sa then steps = Day.sa.toNat - Day.mo.toNat else False⊢ Day.mo ≤ Day.sampr.mo.susteps:Nateq:Std.PRange.succMany? steps Day.mo = some Day.suthis:if Day.mo ≤ Day.su then steps = Day.su.toNat - Day.mo.toNat else False⊢ Day.mo ≤ Day.sumpr.tu.mosteps:Nateq:Std.PRange.succMany? steps Day.tu = some Day.mothis:if Day.tu ≤ Day.mo then steps = Day.mo.toNat - Day.tu.toNat else False⊢ Day.tu ≤ Day.mompr.tu.tusteps:Nateq:Std.PRange.succMany? steps Day.tu = some Day.tuthis:if Day.tu ≤ Day.tu then steps = Day.tu.toNat - Day.tu.toNat else False⊢ Day.tu ≤ Day.tumpr.tu.westeps:Nateq:Std.PRange.succMany? steps Day.tu = some Day.wethis:if Day.tu ≤ Day.we then steps = Day.we.toNat - Day.tu.toNat else False⊢ Day.tu ≤ Day.wempr.tu.thsteps:Nateq:Std.PRange.succMany? steps Day.tu = some Day.ththis:if Day.tu ≤ Day.th then steps = Day.th.toNat - Day.tu.toNat else False⊢ Day.tu ≤ Day.thmpr.tu.frsteps:Nateq:Std.PRange.succMany? steps Day.tu = some Day.frthis:if Day.tu ≤ Day.fr then steps = Day.fr.toNat - Day.tu.toNat else False⊢ Day.tu ≤ Day.frmpr.tu.sasteps:Nateq:Std.PRange.succMany? steps Day.tu = some Day.sathis:if Day.tu ≤ Day.sa then steps = Day.sa.toNat - Day.tu.toNat else False⊢ Day.tu ≤ Day.sampr.tu.susteps:Nateq:Std.PRange.succMany? steps Day.tu = some Day.suthis:if Day.tu ≤ Day.su then steps = Day.su.toNat - Day.tu.toNat else False⊢ Day.tu ≤ Day.sumpr.we.mosteps:Nateq:Std.PRange.succMany? steps Day.we = some Day.mothis:if Day.we ≤ Day.mo then steps = Day.mo.toNat - Day.we.toNat else False⊢ Day.we ≤ Day.mompr.we.tusteps:Nateq:Std.PRange.succMany? steps Day.we = some Day.tuthis:if Day.we ≤ Day.tu then steps = Day.tu.toNat - Day.we.toNat else False⊢ Day.we ≤ Day.tumpr.we.westeps:Nateq:Std.PRange.succMany? steps Day.we = some Day.wethis:if Day.we ≤ Day.we then steps = Day.we.toNat - Day.we.toNat else False⊢ Day.we ≤ Day.wempr.we.thsteps:Nateq:Std.PRange.succMany? steps Day.we = some Day.ththis:if Day.we ≤ Day.th then steps = Day.th.toNat - Day.we.toNat else False⊢ Day.we ≤ Day.thmpr.we.frsteps:Nateq:Std.PRange.succMany? steps Day.we = some Day.frthis:if Day.we ≤ Day.fr then steps = Day.fr.toNat - Day.we.toNat else False⊢ Day.we ≤ Day.frmpr.we.sasteps:Nateq:Std.PRange.succMany? steps Day.we = some Day.sathis:if Day.we ≤ Day.sa then steps = Day.sa.toNat - Day.we.toNat else False⊢ Day.we ≤ Day.sampr.we.susteps:Nateq:Std.PRange.succMany? steps Day.we = some Day.suthis:if Day.we ≤ Day.su then steps = Day.su.toNat - Day.we.toNat else False⊢ Day.we ≤ Day.sumpr.th.mosteps:Nateq:Std.PRange.succMany? steps Day.th = some Day.mothis:if Day.th ≤ Day.mo then steps = Day.mo.toNat - Day.th.toNat else False⊢ Day.th ≤ Day.mompr.th.tusteps:Nateq:Std.PRange.succMany? steps Day.th = some Day.tuthis:if Day.th ≤ Day.tu then steps = Day.tu.toNat - Day.th.toNat else False⊢ Day.th ≤ Day.tumpr.th.westeps:Nateq:Std.PRange.succMany? steps Day.th = some Day.wethis:if Day.th ≤ Day.we then steps = Day.we.toNat - Day.th.toNat else False⊢ Day.th ≤ Day.wempr.th.thsteps:Nateq:Std.PRange.succMany? steps Day.th = some Day.ththis:if Day.th ≤ Day.th then steps = Day.th.toNat - Day.th.toNat else False⊢ Day.th ≤ Day.thmpr.th.frsteps:Nateq:Std.PRange.succMany? steps Day.th = some Day.frthis:if Day.th ≤ Day.fr then steps = Day.fr.toNat - Day.th.toNat else False⊢ Day.th ≤ Day.frmpr.th.sasteps:Nateq:Std.PRange.succMany? steps Day.th = some Day.sathis:if Day.th ≤ Day.sa then steps = Day.sa.toNat - Day.th.toNat else False⊢ Day.th ≤ Day.sampr.th.susteps:Nateq:Std.PRange.succMany? steps Day.th = some Day.suthis:if Day.th ≤ Day.su then steps = Day.su.toNat - Day.th.toNat else False⊢ Day.th ≤ Day.sumpr.fr.mosteps:Nateq:Std.PRange.succMany? steps Day.fr = some Day.mothis:if Day.fr ≤ Day.mo then steps = Day.mo.toNat - Day.fr.toNat else False⊢ Day.fr ≤ Day.mompr.fr.tusteps:Nateq:Std.PRange.succMany? steps Day.fr = some Day.tuthis:if Day.fr ≤ Day.tu then steps = Day.tu.toNat - Day.fr.toNat else False⊢ Day.fr ≤ Day.tumpr.fr.westeps:Nateq:Std.PRange.succMany? steps Day.fr = some Day.wethis:if Day.fr ≤ Day.we then steps = Day.we.toNat - Day.fr.toNat else False⊢ Day.fr ≤ Day.wempr.fr.thsteps:Nateq:Std.PRange.succMany? steps Day.fr = some Day.ththis:if Day.fr ≤ Day.th then steps = Day.th.toNat - Day.fr.toNat else False⊢ Day.fr ≤ Day.thmpr.fr.frsteps:Nateq:Std.PRange.succMany? steps Day.fr = some Day.frthis:if Day.fr ≤ Day.fr then steps = Day.fr.toNat - Day.fr.toNat else False⊢ Day.fr ≤ Day.frmpr.fr.sasteps:Nateq:Std.PRange.succMany? steps Day.fr = some Day.sathis:if Day.fr ≤ Day.sa then steps = Day.sa.toNat - Day.fr.toNat else False⊢ Day.fr ≤ Day.sampr.fr.susteps:Nateq:Std.PRange.succMany? steps Day.fr = some Day.suthis:if Day.fr ≤ Day.su then steps = Day.su.toNat - Day.fr.toNat else False⊢ Day.fr ≤ Day.sumpr.sa.mosteps:Nateq:Std.PRange.succMany? steps Day.sa = some Day.mothis:if Day.sa ≤ Day.mo then steps = Day.mo.toNat - Day.sa.toNat else False⊢ Day.sa ≤ Day.mompr.sa.tusteps:Nateq:Std.PRange.succMany? steps Day.sa = some Day.tuthis:if Day.sa ≤ Day.tu then steps = Day.tu.toNat - Day.sa.toNat else False⊢ Day.sa ≤ Day.tumpr.sa.westeps:Nateq:Std.PRange.succMany? steps Day.sa = some Day.wethis:if Day.sa ≤ Day.we then steps = Day.we.toNat - Day.sa.toNat else False⊢ Day.sa ≤ Day.wempr.sa.thsteps:Nateq:Std.PRange.succMany? steps Day.sa = some Day.ththis:if Day.sa ≤ Day.th then steps = Day.th.toNat - Day.sa.toNat else False⊢ Day.sa ≤ Day.thmpr.sa.frsteps:Nateq:Std.PRange.succMany? steps Day.sa = some Day.frthis:if Day.sa ≤ Day.fr then steps = Day.fr.toNat - Day.sa.toNat else False⊢ Day.sa ≤ Day.frmpr.sa.sasteps:Nateq:Std.PRange.succMany? steps Day.sa = some Day.sathis:if Day.sa ≤ Day.sa then steps = Day.sa.toNat - Day.sa.toNat else False⊢ Day.sa ≤ Day.sampr.sa.susteps:Nateq:Std.PRange.succMany? steps Day.sa = some Day.suthis:if Day.sa ≤ Day.su then steps = Day.su.toNat - Day.sa.toNat else False⊢ Day.sa ≤ Day.sumpr.su.mosteps:Nateq:Std.PRange.succMany? steps Day.su = some Day.mothis:if Day.su ≤ Day.mo then steps = Day.mo.toNat - Day.su.toNat else False⊢ Day.su ≤ Day.mompr.su.tusteps:Nateq:Std.PRange.succMany? steps Day.su = some Day.tuthis:if Day.su ≤ Day.tu then steps = Day.tu.toNat - Day.su.toNat else False⊢ Day.su ≤ Day.tumpr.su.westeps:Nateq:Std.PRange.succMany? steps Day.su = some Day.wethis:if Day.su ≤ Day.we then steps = Day.we.toNat - Day.su.toNat else False⊢ Day.su ≤ Day.wempr.su.thsteps:Nateq:Std.PRange.succMany? steps Day.su = some Day.ththis:if Day.su ≤ Day.th then steps = Day.th.toNat - Day.su.toNat else False⊢ Day.su ≤ Day.thmpr.su.frsteps:Nateq:Std.PRange.succMany? steps Day.su = some Day.frthis:if Day.su ≤ Day.fr then steps = Day.fr.toNat - Day.su.toNat else False⊢ Day.su ≤ Day.frmpr.su.sasteps:Nateq:Std.PRange.succMany? steps Day.su = some Day.sathis:if Day.su ≤ Day.sa then steps = Day.sa.toNat - Day.su.toNat else False⊢ Day.su ≤ Day.sampr.su.susteps:Nateq:Std.PRange.succMany? steps Day.su = some Day.suthis:if Day.su ≤ Day.su then steps = Day.su.toNat - Day.su.toNat else False⊢ Day.su ≤ Day.su
      simp only [`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` instead`if_false_right` has been deprecated: Use `ite_false_right` insteadif_false_right] at thismpr.su.susteps:Nateq:Std.PRange.succMany? steps Day.su = some Day.suthis:Day.su ≤ Day.su ∧ steps = Day.su.toNat - Day.su.toNat⊢ Day.su ≤ Day.su <;>mpr.mo.mosteps:Nateq:Std.PRange.succMany? steps Day.mo = some Day.mothis:Day.mo ≤ Day.mo ∧ steps = Day.mo.toNat - Day.mo.toNat⊢ Day.mo ≤ Day.mompr.mo.tusteps:Nateq:Std.PRange.succMany? steps Day.mo = some Day.tuthis:Day.mo ≤ Day.tu ∧ steps = Day.tu.toNat - Day.mo.toNat⊢ Day.mo ≤ Day.tumpr.mo.westeps:Nateq:Std.PRange.succMany? steps Day.mo = some Day.wethis:Day.mo ≤ Day.we ∧ steps = Day.we.toNat - Day.mo.toNat⊢ Day.mo ≤ Day.wempr.mo.thsteps:Nateq:Std.PRange.succMany? steps Day.mo = some Day.ththis:Day.mo ≤ Day.th ∧ steps = Day.th.toNat - Day.mo.toNat⊢ Day.mo ≤ Day.thmpr.mo.frsteps:Nateq:Std.PRange.succMany? steps Day.mo = some Day.frthis:Day.mo ≤ Day.fr ∧ steps = Day.fr.toNat - Day.mo.toNat⊢ Day.mo ≤ Day.frmpr.mo.sasteps:Nateq:Std.PRange.succMany? steps Day.mo = some Day.sathis:Day.mo ≤ Day.sa ∧ steps = Day.sa.toNat - Day.mo.toNat⊢ Day.mo ≤ Day.sampr.mo.susteps:Nateq:Std.PRange.succMany? steps Day.mo = some Day.suthis:Day.mo ≤ Day.su ∧ steps = Day.su.toNat - Day.mo.toNat⊢ Day.mo ≤ Day.sumpr.tu.mosteps:Nateq:Std.PRange.succMany? steps Day.tu = some Day.mothis:Day.tu ≤ Day.mo ∧ steps = Day.mo.toNat - Day.tu.toNat⊢ Day.tu ≤ Day.mompr.tu.tusteps:Nateq:Std.PRange.succMany? steps Day.tu = some Day.tuthis:Day.tu ≤ Day.tu ∧ steps = Day.tu.toNat - Day.tu.toNat⊢ Day.tu ≤ Day.tumpr.tu.westeps:Nateq:Std.PRange.succMany? steps Day.tu = some Day.wethis:Day.tu ≤ Day.we ∧ steps = Day.we.toNat - Day.tu.toNat⊢ Day.tu ≤ Day.wempr.tu.thsteps:Nateq:Std.PRange.succMany? steps Day.tu = some Day.ththis:Day.tu ≤ Day.th ∧ steps = Day.th.toNat - Day.tu.toNat⊢ Day.tu ≤ Day.thmpr.tu.frsteps:Nateq:Std.PRange.succMany? steps Day.tu = some Day.frthis:Day.tu ≤ Day.fr ∧ steps = Day.fr.toNat - Day.tu.toNat⊢ Day.tu ≤ Day.frmpr.tu.sasteps:Nateq:Std.PRange.succMany? steps Day.tu = some Day.sathis:Day.tu ≤ Day.sa ∧ steps = Day.sa.toNat - Day.tu.toNat⊢ Day.tu ≤ Day.sampr.tu.susteps:Nateq:Std.PRange.succMany? steps Day.tu = some Day.suthis:Day.tu ≤ Day.su ∧ steps = Day.su.toNat - Day.tu.toNat⊢ Day.tu ≤ Day.sumpr.we.mosteps:Nateq:Std.PRange.succMany? steps Day.we = some Day.mothis:Day.we ≤ Day.mo ∧ steps = Day.mo.toNat - Day.we.toNat⊢ Day.we ≤ Day.mompr.we.tusteps:Nateq:Std.PRange.succMany? steps Day.we = some Day.tuthis:Day.we ≤ Day.tu ∧ steps = Day.tu.toNat - Day.we.toNat⊢ Day.we ≤ Day.tumpr.we.westeps:Nateq:Std.PRange.succMany? steps Day.we = some Day.wethis:Day.we ≤ Day.we ∧ steps = Day.we.toNat - Day.we.toNat⊢ Day.we ≤ Day.wempr.we.thsteps:Nateq:Std.PRange.succMany? steps Day.we = some Day.ththis:Day.we ≤ Day.th ∧ steps = Day.th.toNat - Day.we.toNat⊢ Day.we ≤ Day.thmpr.we.frsteps:Nateq:Std.PRange.succMany? steps Day.we = some Day.frthis:Day.we ≤ Day.fr ∧ steps = Day.fr.toNat - Day.we.toNat⊢ Day.we ≤ Day.frmpr.we.sasteps:Nateq:Std.PRange.succMany? steps Day.we = some Day.sathis:Day.we ≤ Day.sa ∧ steps = Day.sa.toNat - Day.we.toNat⊢ Day.we ≤ Day.sampr.we.susteps:Nateq:Std.PRange.succMany? steps Day.we = some Day.suthis:Day.we ≤ Day.su ∧ steps = Day.su.toNat - Day.we.toNat⊢ Day.we ≤ Day.sumpr.th.mosteps:Nateq:Std.PRange.succMany? steps Day.th = some Day.mothis:Day.th ≤ Day.mo ∧ steps = Day.mo.toNat - Day.th.toNat⊢ Day.th ≤ Day.mompr.th.tusteps:Nateq:Std.PRange.succMany? steps Day.th = some Day.tuthis:Day.th ≤ Day.tu ∧ steps = Day.tu.toNat - Day.th.toNat⊢ Day.th ≤ Day.tumpr.th.westeps:Nateq:Std.PRange.succMany? steps Day.th = some Day.wethis:Day.th ≤ Day.we ∧ steps = Day.we.toNat - Day.th.toNat⊢ Day.th ≤ Day.wempr.th.thsteps:Nateq:Std.PRange.succMany? steps Day.th = some Day.ththis:Day.th ≤ Day.th ∧ steps = Day.th.toNat - Day.th.toNat⊢ Day.th ≤ Day.thmpr.th.frsteps:Nateq:Std.PRange.succMany? steps Day.th = some Day.frthis:Day.th ≤ Day.fr ∧ steps = Day.fr.toNat - Day.th.toNat⊢ Day.th ≤ Day.frmpr.th.sasteps:Nateq:Std.PRange.succMany? steps Day.th = some Day.sathis:Day.th ≤ Day.sa ∧ steps = Day.sa.toNat - Day.th.toNat⊢ Day.th ≤ Day.sampr.th.susteps:Nateq:Std.PRange.succMany? steps Day.th = some Day.suthis:Day.th ≤ Day.su ∧ steps = Day.su.toNat - Day.th.toNat⊢ Day.th ≤ Day.sumpr.fr.mosteps:Nateq:Std.PRange.succMany? steps Day.fr = some Day.mothis:Day.fr ≤ Day.mo ∧ steps = Day.mo.toNat - Day.fr.toNat⊢ Day.fr ≤ Day.mompr.fr.tusteps:Nateq:Std.PRange.succMany? steps Day.fr = some Day.tuthis:Day.fr ≤ Day.tu ∧ steps = Day.tu.toNat - Day.fr.toNat⊢ Day.fr ≤ Day.tumpr.fr.westeps:Nateq:Std.PRange.succMany? steps Day.fr = some Day.wethis:Day.fr ≤ Day.we ∧ steps = Day.we.toNat - Day.fr.toNat⊢ Day.fr ≤ Day.wempr.fr.thsteps:Nateq:Std.PRange.succMany? steps Day.fr = some Day.ththis:Day.fr ≤ Day.th ∧ steps = Day.th.toNat - Day.fr.toNat⊢ Day.fr ≤ Day.thmpr.fr.frsteps:Nateq:Std.PRange.succMany? steps Day.fr = some Day.frthis:Day.fr ≤ Day.fr ∧ steps = Day.fr.toNat - Day.fr.toNat⊢ Day.fr ≤ Day.frmpr.fr.sasteps:Nateq:Std.PRange.succMany? steps Day.fr = some Day.sathis:Day.fr ≤ Day.sa ∧ steps = Day.sa.toNat - Day.fr.toNat⊢ Day.fr ≤ Day.sampr.fr.susteps:Nateq:Std.PRange.succMany? steps Day.fr = some Day.suthis:Day.fr ≤ Day.su ∧ steps = Day.su.toNat - Day.fr.toNat⊢ Day.fr ≤ Day.sumpr.sa.mosteps:Nateq:Std.PRange.succMany? steps Day.sa = some Day.mothis:Day.sa ≤ Day.mo ∧ steps = Day.mo.toNat - Day.sa.toNat⊢ Day.sa ≤ Day.mompr.sa.tusteps:Nateq:Std.PRange.succMany? steps Day.sa = some Day.tuthis:Day.sa ≤ Day.tu ∧ steps = Day.tu.toNat - Day.sa.toNat⊢ Day.sa ≤ Day.tumpr.sa.westeps:Nateq:Std.PRange.succMany? steps Day.sa = some Day.wethis:Day.sa ≤ Day.we ∧ steps = Day.we.toNat - Day.sa.toNat⊢ Day.sa ≤ Day.wempr.sa.thsteps:Nateq:Std.PRange.succMany? steps Day.sa = some Day.ththis:Day.sa ≤ Day.th ∧ steps = Day.th.toNat - Day.sa.toNat⊢ Day.sa ≤ Day.thmpr.sa.frsteps:Nateq:Std.PRange.succMany? steps Day.sa = some Day.frthis:Day.sa ≤ Day.fr ∧ steps = Day.fr.toNat - Day.sa.toNat⊢ Day.sa ≤ Day.frmpr.sa.sasteps:Nateq:Std.PRange.succMany? steps Day.sa = some Day.sathis:Day.sa ≤ Day.sa ∧ steps = Day.sa.toNat - Day.sa.toNat⊢ Day.sa ≤ Day.sampr.sa.susteps:Nateq:Std.PRange.succMany? steps Day.sa = some Day.suthis:Day.sa ≤ Day.su ∧ steps = Day.su.toNat - Day.sa.toNat⊢ Day.sa ≤ Day.sumpr.su.mosteps:Nateq:Std.PRange.succMany? steps Day.su = some Day.mothis:Day.su ≤ Day.mo ∧ steps = Day.mo.toNat - Day.su.toNat⊢ Day.su ≤ Day.mompr.su.tusteps:Nateq:Std.PRange.succMany? steps Day.su = some Day.tuthis:Day.su ≤ Day.tu ∧ steps = Day.tu.toNat - Day.su.toNat⊢ Day.su ≤ Day.tumpr.su.westeps:Nateq:Std.PRange.succMany? steps Day.su = some Day.wethis:Day.su ≤ Day.we ∧ steps = Day.we.toNat - Day.su.toNat⊢ Day.su ≤ Day.wempr.su.thsteps:Nateq:Std.PRange.succMany? steps Day.su = some Day.ththis:Day.su ≤ Day.th ∧ steps = Day.th.toNat - Day.su.toNat⊢ Day.su ≤ Day.thmpr.su.frsteps:Nateq:Std.PRange.succMany? steps Day.su = some Day.frthis:Day.su ≤ Day.fr ∧ steps = Day.fr.toNat - Day.su.toNat⊢ Day.su ≤ Day.frmpr.su.sasteps:Nateq:Std.PRange.succMany? steps Day.su = some Day.sathis:Day.su ≤ Day.sa ∧ steps = Day.sa.toNat - Day.su.toNat⊢ Day.su ≤ Day.sampr.su.susteps:Nateq:Std.PRange.succMany? steps Day.su = some Day.suthis:Day.su ≤ Day.su ∧ steps = Day.su.toNat - Day.su.toNat⊢ Day.su ≤ Day.su
      cases thismpr.su.su.introsteps:Nateq:Std.PRange.succMany? steps Day.su = some Day.suleft✝:Day.su ≤ Day.suright✝:steps = Day.su.toNat - Day.su.toNat⊢ Day.su ≤ Day.su <;>mpr.mo.mo.introsteps:Nateq:Std.PRange.succMany? steps Day.mo = some Day.moleft✝:Day.mo ≤ Day.moright✝:steps = Day.mo.toNat - Day.mo.toNat⊢ Day.mo ≤ Day.mompr.mo.tu.introsteps:Nateq:Std.PRange.succMany? steps Day.mo = some Day.tuleft✝:Day.mo ≤ Day.turight✝:steps = Day.tu.toNat - Day.mo.toNat⊢ Day.mo ≤ Day.tumpr.mo.we.introsteps:Nateq:Std.PRange.succMany? steps Day.mo = some Day.weleft✝:Day.mo ≤ Day.weright✝:steps = Day.we.toNat - Day.mo.toNat⊢ Day.mo ≤ Day.wempr.mo.th.introsteps:Nateq:Std.PRange.succMany? steps Day.mo = some Day.thleft✝:Day.mo ≤ Day.thright✝:steps = Day.th.toNat - Day.mo.toNat⊢ Day.mo ≤ Day.thmpr.mo.fr.introsteps:Nateq:Std.PRange.succMany? steps Day.mo = some Day.frleft✝:Day.mo ≤ Day.frright✝:steps = Day.fr.toNat - Day.mo.toNat⊢ Day.mo ≤ Day.frmpr.mo.sa.introsteps:Nateq:Std.PRange.succMany? steps Day.mo = some Day.saleft✝:Day.mo ≤ Day.saright✝:steps = Day.sa.toNat - Day.mo.toNat⊢ Day.mo ≤ Day.sampr.mo.su.introsteps:Nateq:Std.PRange.succMany? steps Day.mo = some Day.suleft✝:Day.mo ≤ Day.suright✝:steps = Day.su.toNat - Day.mo.toNat⊢ Day.mo ≤ Day.sumpr.tu.mo.introsteps:Nateq:Std.PRange.succMany? steps Day.tu = some Day.moleft✝:Day.tu ≤ Day.moright✝:steps = Day.mo.toNat - Day.tu.toNat⊢ Day.tu ≤ Day.mompr.tu.tu.introsteps:Nateq:Std.PRange.succMany? steps Day.tu = some Day.tuleft✝:Day.tu ≤ Day.turight✝:steps = Day.tu.toNat - Day.tu.toNat⊢ Day.tu ≤ Day.tumpr.tu.we.introsteps:Nateq:Std.PRange.succMany? steps Day.tu = some Day.weleft✝:Day.tu ≤ Day.weright✝:steps = Day.we.toNat - Day.tu.toNat⊢ Day.tu ≤ Day.wempr.tu.th.introsteps:Nateq:Std.PRange.succMany? steps Day.tu = some Day.thleft✝:Day.tu ≤ Day.thright✝:steps = Day.th.toNat - Day.tu.toNat⊢ Day.tu ≤ Day.thmpr.tu.fr.introsteps:Nateq:Std.PRange.succMany? steps Day.tu = some Day.frleft✝:Day.tu ≤ Day.frright✝:steps = Day.fr.toNat - Day.tu.toNat⊢ Day.tu ≤ Day.frmpr.tu.sa.introsteps:Nateq:Std.PRange.succMany? steps Day.tu = some Day.saleft✝:Day.tu ≤ Day.saright✝:steps = Day.sa.toNat - Day.tu.toNat⊢ Day.tu ≤ Day.sampr.tu.su.introsteps:Nateq:Std.PRange.succMany? steps Day.tu = some Day.suleft✝:Day.tu ≤ Day.suright✝:steps = Day.su.toNat - Day.tu.toNat⊢ Day.tu ≤ Day.sumpr.we.mo.introsteps:Nateq:Std.PRange.succMany? steps Day.we = some Day.moleft✝:Day.we ≤ Day.moright✝:steps = Day.mo.toNat - Day.we.toNat⊢ Day.we ≤ Day.mompr.we.tu.introsteps:Nateq:Std.PRange.succMany? steps Day.we = some Day.tuleft✝:Day.we ≤ Day.turight✝:steps = Day.tu.toNat - Day.we.toNat⊢ Day.we ≤ Day.tumpr.we.we.introsteps:Nateq:Std.PRange.succMany? steps Day.we = some Day.weleft✝:Day.we ≤ Day.weright✝:steps = Day.we.toNat - Day.we.toNat⊢ Day.we ≤ Day.wempr.we.th.introsteps:Nateq:Std.PRange.succMany? steps Day.we = some Day.thleft✝:Day.we ≤ Day.thright✝:steps = Day.th.toNat - Day.we.toNat⊢ Day.we ≤ Day.thmpr.we.fr.introsteps:Nateq:Std.PRange.succMany? steps Day.we = some Day.frleft✝:Day.we ≤ Day.frright✝:steps = Day.fr.toNat - Day.we.toNat⊢ Day.we ≤ Day.frmpr.we.sa.introsteps:Nateq:Std.PRange.succMany? steps Day.we = some Day.saleft✝:Day.we ≤ Day.saright✝:steps = Day.sa.toNat - Day.we.toNat⊢ Day.we ≤ Day.sampr.we.su.introsteps:Nateq:Std.PRange.succMany? steps Day.we = some Day.suleft✝:Day.we ≤ Day.suright✝:steps = Day.su.toNat - Day.we.toNat⊢ Day.we ≤ Day.sumpr.th.mo.introsteps:Nateq:Std.PRange.succMany? steps Day.th = some Day.moleft✝:Day.th ≤ Day.moright✝:steps = Day.mo.toNat - Day.th.toNat⊢ Day.th ≤ Day.mompr.th.tu.introsteps:Nateq:Std.PRange.succMany? steps Day.th = some Day.tuleft✝:Day.th ≤ Day.turight✝:steps = Day.tu.toNat - Day.th.toNat⊢ Day.th ≤ Day.tumpr.th.we.introsteps:Nateq:Std.PRange.succMany? steps Day.th = some Day.weleft✝:Day.th ≤ Day.weright✝:steps = Day.we.toNat - Day.th.toNat⊢ Day.th ≤ Day.wempr.th.th.introsteps:Nateq:Std.PRange.succMany? steps Day.th = some Day.thleft✝:Day.th ≤ Day.thright✝:steps = Day.th.toNat - Day.th.toNat⊢ Day.th ≤ Day.thmpr.th.fr.introsteps:Nateq:Std.PRange.succMany? steps Day.th = some Day.frleft✝:Day.th ≤ Day.frright✝:steps = Day.fr.toNat - Day.th.toNat⊢ Day.th ≤ Day.frmpr.th.sa.introsteps:Nateq:Std.PRange.succMany? steps Day.th = some Day.saleft✝:Day.th ≤ Day.saright✝:steps = Day.sa.toNat - Day.th.toNat⊢ Day.th ≤ Day.sampr.th.su.introsteps:Nateq:Std.PRange.succMany? steps Day.th = some Day.suleft✝:Day.th ≤ Day.suright✝:steps = Day.su.toNat - Day.th.toNat⊢ Day.th ≤ Day.sumpr.fr.mo.introsteps:Nateq:Std.PRange.succMany? steps Day.fr = some Day.moleft✝:Day.fr ≤ Day.moright✝:steps = Day.mo.toNat - Day.fr.toNat⊢ Day.fr ≤ Day.mompr.fr.tu.introsteps:Nateq:Std.PRange.succMany? steps Day.fr = some Day.tuleft✝:Day.fr ≤ Day.turight✝:steps = Day.tu.toNat - Day.fr.toNat⊢ Day.fr ≤ Day.tumpr.fr.we.introsteps:Nateq:Std.PRange.succMany? steps Day.fr = some Day.weleft✝:Day.fr ≤ Day.weright✝:steps = Day.we.toNat - Day.fr.toNat⊢ Day.fr ≤ Day.wempr.fr.th.introsteps:Nateq:Std.PRange.succMany? steps Day.fr = some Day.thleft✝:Day.fr ≤ Day.thright✝:steps = Day.th.toNat - Day.fr.toNat⊢ Day.fr ≤ Day.thmpr.fr.fr.introsteps:Nateq:Std.PRange.succMany? steps Day.fr = some Day.frleft✝:Day.fr ≤ Day.frright✝:steps = Day.fr.toNat - Day.fr.toNat⊢ Day.fr ≤ Day.frmpr.fr.sa.introsteps:Nateq:Std.PRange.succMany? steps Day.fr = some Day.saleft✝:Day.fr ≤ Day.saright✝:steps = Day.sa.toNat - Day.fr.toNat⊢ Day.fr ≤ Day.sampr.fr.su.introsteps:Nateq:Std.PRange.succMany? steps Day.fr = some Day.suleft✝:Day.fr ≤ Day.suright✝:steps = Day.su.toNat - Day.fr.toNat⊢ Day.fr ≤ Day.sumpr.sa.mo.introsteps:Nateq:Std.PRange.succMany? steps Day.sa = some Day.moleft✝:Day.sa ≤ Day.moright✝:steps = Day.mo.toNat - Day.sa.toNat⊢ Day.sa ≤ Day.mompr.sa.tu.introsteps:Nateq:Std.PRange.succMany? steps Day.sa = some Day.tuleft✝:Day.sa ≤ Day.turight✝:steps = Day.tu.toNat - Day.sa.toNat⊢ Day.sa ≤ Day.tumpr.sa.we.introsteps:Nateq:Std.PRange.succMany? steps Day.sa = some Day.weleft✝:Day.sa ≤ Day.weright✝:steps = Day.we.toNat - Day.sa.toNat⊢ Day.sa ≤ Day.wempr.sa.th.introsteps:Nateq:Std.PRange.succMany? steps Day.sa = some Day.thleft✝:Day.sa ≤ Day.thright✝:steps = Day.th.toNat - Day.sa.toNat⊢ Day.sa ≤ Day.thmpr.sa.fr.introsteps:Nateq:Std.PRange.succMany? steps Day.sa = some Day.frleft✝:Day.sa ≤ Day.frright✝:steps = Day.fr.toNat - Day.sa.toNat⊢ Day.sa ≤ Day.frmpr.sa.sa.introsteps:Nateq:Std.PRange.succMany? steps Day.sa = some Day.saleft✝:Day.sa ≤ Day.saright✝:steps = Day.sa.toNat - Day.sa.toNat⊢ Day.sa ≤ Day.sampr.sa.su.introsteps:Nateq:Std.PRange.succMany? steps Day.sa = some Day.suleft✝:Day.sa ≤ Day.suright✝:steps = Day.su.toNat - Day.sa.toNat⊢ Day.sa ≤ Day.sumpr.su.mo.introsteps:Nateq:Std.PRange.succMany? steps Day.su = some Day.moleft✝:Day.su ≤ Day.moright✝:steps = Day.mo.toNat - Day.su.toNat⊢ Day.su ≤ Day.mompr.su.tu.introsteps:Nateq:Std.PRange.succMany? steps Day.su = some Day.tuleft✝:Day.su ≤ Day.turight✝:steps = Day.tu.toNat - Day.su.toNat⊢ Day.su ≤ Day.tumpr.su.we.introsteps:Nateq:Std.PRange.succMany? steps Day.su = some Day.weleft✝:Day.su ≤ Day.weright✝:steps = Day.we.toNat - Day.su.toNat⊢ Day.su ≤ Day.wempr.su.th.introsteps:Nateq:Std.PRange.succMany? steps Day.su = some Day.thleft✝:Day.su ≤ Day.thright✝:steps = Day.th.toNat - Day.su.toNat⊢ Day.su ≤ Day.thmpr.su.fr.introsteps:Nateq:Std.PRange.succMany? steps Day.su = some Day.frleft✝:Day.su ≤ Day.frright✝:steps = Day.fr.toNat - Day.su.toNat⊢ Day.su ≤ Day.frmpr.su.sa.introsteps:Nateq:Std.PRange.succMany? steps Day.su = some Day.saleft✝:Day.su ≤ Day.saright✝:steps = Day.sa.toNat - Day.su.toNat⊢ Day.su ≤ Day.sampr.su.su.introsteps:Nateq:Std.PRange.succMany? steps Day.su = some Day.suleft✝:Day.su ≤ Day.suright✝:steps = Day.su.toNat - Day.su.toNat⊢ Day.su ≤ Day.su grindAll goals completed! 🐙

现在就可以在天的范围上进行迭代了：

It's Day.mo
It's Day.tu
It's Day.we
#eval show IO Unit from do
  for x in (Day.mo...Day.th).iter do
    IO.println s!"It's {repr x}"

It's Day.mo
It's Day.tu
It's Day.we

在线查看 ↪

20.18.4. 范围与切片🔗

范围语法可与支持切片的数据结构结合使用，以选择结构的一个切片。

列表切片

列表可以使用任何区间类型进行切片：

def groceries :=
  ["apples", "bananas", "coffee", "dates", "endive", "fennel"]

["bananas", "coffee", "dates"]#eval groceries[1...4] |>.toList

["bananas", "coffee", "dates"]

["bananas", "coffee", "dates", "endive"]#eval groceries[1...=4] |>.toList

["bananas", "coffee", "dates", "endive"]

["bananas", "coffee", "dates", "endive", "fennel"]#eval groceries[1...*] |>.toList

["bananas", "coffee", "dates", "endive", "fennel"]

["coffee", "dates"]#eval groceries[1<...4] |>.toList

["coffee", "dates"]

["coffee", "dates", "endive"]#eval groceries[1<...=4] |>.toList

["coffee", "dates", "endive"]

["apples", "bananas", "coffee", "dates", "endive"]#eval groceries[*...=4] |>.toList

["apples", "bananas", "coffee", "dates", "endive"]

["apples", "bananas", "coffee", "dates"]#eval groceries[*...4] |>.toList

["apples", "bananas", "coffee", "dates"]

["apples", "bananas", "coffee", "dates", "endive", "fennel"]#eval groceries[*...*] |>.toList

["apples", "bananas", "coffee", "dates", "endive", "fennel"]

在线查看 ↪

自定义切片

Triple 包含三个相同类型的值：

structure Triple (α : Type u) where
  fst : α
  snd : α
  thd : α
deriving Repr

在三元组中的位置可以是任何字段，或就在 thd 之后：

inductive TriplePos where
  | fst | snd | thd | done
deriving Repr

三元组的切片由三元组、起始位置和停止位置组成。起始位置包含在范围内，停止位置不包含在范围内：

structure TripleSlice (α : Type u) where
  triple : Triple α
  start : TriplePos
  stop : TriplePos
deriving Repr

TriplePos 的范围可用于从三元组中选择切片，方法是为每种受支持的范围类型实现 Sliceable 类的实例。例如，Std.Rco.Sliceable 允许左闭右开范围被用来对 Triple 进行切片：

instance : Std.Rco.Sliceable (Triple α) TriplePos (TripleSlice α) where
  mkSlice triple range :=
    { triple, start := range.lower, stop := range.upper }

def abc : Triple Char := ⟨'a', 'b', 'c'⟩

open TriplePos in
{ triple := { fst := 'a', snd := 'b', thd := 'c' }, start := TriplePos.snd, stop := TriplePos.thd }#eval abc[snd...thd]

{ triple := { fst := 'a', snd := 'b', thd := 'c' }, start := TriplePos.snd, stop := TriplePos.thd }

无限范围只有下界：

instance : Std.Rci.Sliceable (Triple α) TriplePos (TripleSlice α) where
  mkSlice triple range :=
    { triple, start := range.lower, stop := .done }

open TriplePos in
{ triple := { fst := 'a', snd := 'b', thd := 'c' }, start := TriplePos.snd, stop := TriplePos.done }#eval abc[snd...*]

{ triple := { fst := 'a', snd := 'b', thd := 'c' }, start := TriplePos.snd, stop := TriplePos.done }

在线查看 ↪

类型类

Std.Rco.Sliceable.{u, v, w} (α : Type u) (β : outParam (Type v))
  (γ : outParam (Type w)) : Type (max (max u v) w)
Std.Rco.Sliceable.{u, v, w} (α : Type u)
  (β : outParam (Type v))
  (γ : outParam (Type w)) :
  Type (max (max u v) w)

此类型类说明如何取得 α 中元素；这些切片由索引类型 β 中的左闭右开区间指定。

结果切片的类型为 γ。

实例构造子

Std.Rco.Sliceable.mk.{u, v, w}

方法

mkSlice : α → Std.Rco β → γ

将 carrier 切取为从 range.lower（含）到 range.upper（不含）的切片。

类型类

Std.Rcc.Sliceable.{u, v, w} (α : Type u) (β : outParam (Type v))
  (γ : outParam (Type w)) : Type (max (max u v) w)
Std.Rcc.Sliceable.{u, v, w} (α : Type u)
  (β : outParam (Type v))
  (γ : outParam (Type w)) :
  Type (max (max u v) w)

这个类型类表示如何获取α中元素在索引类型β范围上的切片，这些范围是闭合的。

结果切片的类型是 γ。

实例构造子

Std.Rcc.Sliceable.mk.{u, v, w}

方法

mkSlice : α → Std.Rcc β → γ

将 carrier 切取为从 range.lower 到 range.upper（两端均含）的切片。

类型类

Std.Rci.Sliceable.{u, v, w} (α : Type u) (β : outParam (Type v))
  (γ : outParam (Type w)) : Type (max (max u v) w)
Std.Rci.Sliceable.{u, v, w} (α : Type u)
  (β : outParam (Type v))
  (γ : outParam (Type w)) :
  Type (max (max u v) w)

此类型类说明如何取得 α 中元素；这些切片由索引类型 β 中左闭、右端无界的区间指定。

结果切片的类型为 γ。

实例构造子

Std.Rci.Sliceable.mk.{u, v, w}

方法

mkSlice : α → Std.Rci β → γ

对 carrier 从 range.lower（含）开始切取。

类型类

Std.Roo.Sliceable.{u, v, w} (α : Type u) (β : outParam (Type v))
  (γ : outParam (Type w)) : Type (max (max u v) w)
Std.Roo.Sliceable.{u, v, w} (α : Type u)
  (β : outParam (Type v))
  (γ : outParam (Type w)) :
  Type (max (max u v) w)

此类型类说明如何取得 α 中元素；这些切片由索引类型 β 中的开区间指定。

结果切片的类型为 γ。

实例构造子

Std.Roo.Sliceable.mk.{u, v, w}

方法

mkSlice : α → Std.Roo β → γ

将 carrier 切取为从 range.lower 到 range.upper（两端均不含）的切片。

类型类

Std.Roc.Sliceable.{u, v, w} (α : Type u) (β : outParam (Type v))
  (γ : outParam (Type w)) : Type (max (max u v) w)
Std.Roc.Sliceable.{u, v, w} (α : Type u)
  (β : outParam (Type v))
  (γ : outParam (Type w)) :
  Type (max (max u v) w)

此类型类说明如何取得 α 中元素；这些切片由索引类型 β 中的左开右闭区间指定。

结果切片的类型为 γ。

实例构造子

Std.Roc.Sliceable.mk.{u, v, w}

方法

mkSlice : α → Std.Roc β → γ

将 carrier 切取为从 range.lower（不含）到 range.upper（含）的切片。

类型类

Std.Roi.Sliceable.{u, v, w} (α : Type u) (β : outParam (Type v))
  (γ : outParam (Type w)) : Type (max (max u v) w)
Std.Roi.Sliceable.{u, v, w} (α : Type u)
  (β : outParam (Type v))
  (γ : outParam (Type w)) :
  Type (max (max u v) w)

此类型类说明如何取得 α 中元素；这些切片由索引类型 β 中左开、右端无界的区间指定。

结果切片的类型为 γ。

实例构造子

Std.Roi.Sliceable.mk.{u, v, w}

方法

mkSlice : α → Std.Roi β → γ

对 carrier 从 range.lower（不含）开始切取。

类型类

Std.Rio.Sliceable.{u, v, w} (α : Type u) (β : outParam (Type v))
  (γ : outParam (Type w)) : Type (max (max u v) w)
Std.Rio.Sliceable.{u, v, w} (α : Type u)
  (β : outParam (Type v))
  (γ : outParam (Type w)) :
  Type (max (max u v) w)

此类型类说明如何取得 α 中元素；这些切片由索引类型 β 中左端无界、右开的区间指定。

结果切片的类型为 γ。

实例构造子

Std.Rio.Sliceable.mk.{u, v, w}

方法

mkSlice : α → Std.Rio β → γ

将 carrier 切取到 range.upper（不含）为止。

类型类

Std.Ric.Sliceable.{u, v, w} (α : Type u) (β : outParam (Type v))
  (γ : outParam (Type w)) : Type (max (max u v) w)
Std.Ric.Sliceable.{u, v, w} (α : Type u)
  (β : outParam (Type v))
  (γ : outParam (Type w)) :
  Type (max (max u v) w)

此类型类说明如何取得 α 中元素；这些切片由索引类型 β 中左端无界、右闭的区间指定。

结果切片的类型为 γ。

实例构造子

Std.Ric.Sliceable.mk.{u, v, w}

方法

mkSlice : α → Std.Ric β → γ

将 carrier 切取到 range.upper（含）为止。

类型类

Std.Rii.Sliceable.{u, v, w} (α : Type u) (β : outParam (Type v))
  (γ : outParam (Type w)) : Type (max u w)
Std.Rii.Sliceable.{u, v, w} (α : Type u)
  (β : outParam (Type v))
  (γ : outParam (Type w)) : Type (max u w)

此类型类说明如何取得 α 中元素；这些切片由索引类型 β 中的全区间指定。

结果切片的类型为 γ。

实例构造子

Std.Rii.Sliceable.mk.{u, v, w}

方法

mkSlice : α → Std.Rii β → γ

切取整个 carrier，不设边界。

20.1.	自然数
20.2.	整数
20.3.	有限自然数
20.4.	定精度整数
20.5.	位向量
20.6.	浮点数
20.7.	字符
20.8.	字符串
20.9.	单元类型
20.10.	空类型
20.11.	布尔值
20.12.	可选值
20.13.	元组
20.14.	和类型
20.15.	链表
20.16.	数组
20.17.	字节数组
20.18.	范围
20.19.	映射与集合
20.20.	子类型
20.21.	惰性计算

20.18. 范围🔗

20.18.1. 范围类型🔗

20.18.2. 范围相关类型类🔗

20.18.3. 实现范围🔗

20.18.4. 范围与切片🔗