The Lean Language Reference

20.18. Ranges🔗

A range represents a series of consecutive elements of some type, from a lower bound to an upper bound. The bounds may be open, in which case the bound value is not part of the range, or closed, in which case the bound value is part of the range. Either bound may be omitted, in which case the range extends infinitely in the corresponding direction.

Ranges have dedicated syntax that consists of a starting point, ..., and an ending point. The starting point may be either *, which denotes a range that continues infinitely downwards, or a term, which denotes a range with a specific starting value. By default, ranges are left-closed: they contain their starting points. A trailing < indicates that the range is left-open and does not contain its starting point. The ending point may be *, in which case the range continues infinitely upwards, or a term, which denotes a range with a specific ending value. By default, ranges are right-open: they do not contain their ending points. The ending point may be prefixed with < to indicate that it is right-open; this is the default and does not change the meaning, but may be easier to read. It may also be prefixed with = to indicate that the range is right-closed and contains its ending point.

Ranges of Natural Numbers

The range that contains the numbers 3 through 6 can be written in a variety of ways:

[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]
Live ↪
Finite and Infinite Ranges

This range cannot be converted to a list, because it is infinite:

#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

Finiteness of a left-closed, right-unbounded range is indicated by the presence of an instance of Std.Rxi.IsAlwaysFinite, which does not exist for Nat. Std.Rco is the type of these ranges, and the name Std.Rxi.IsAlwaysFinite indicates that it determines finiteness for all right-unbounded ranges.

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.

Attempting to enumerate the negative integers leads to a similar error, this time because there is no way to determine the least element:

#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.

Unbounded ranges in finite types indicate that the range extends to the greatest element of the type. Because UInt8 has 256 elements, this range contains 253 elements:

253#eval ((3 : UInt8)...*).toArray.size 
253
Live ↪
syntaxRange Syntax

This range is left-closed, right-open, and indicates Std.Rco:

term ::= ...
    | `a...b` is the range of elements greater than or equal to `a` and less than `b`\.
See also `Std.Rco`\.
term...term

This range is left-closed, right-open, and indicates Std.Rco:

term ::= ...
    | `a...<b` is the range of elements greater than or equal to `a` and less than `b`\.
See also `Std.Rco`\.
term...<term

This range is left-closed, right-closed, and indicates Std.Rcc:

term ::= ...
    | `a...=b` is the range of elements greater than or equal to `a` and less than or equal to
`b`\. See also `Std.Rcc`\.
term...=term

This range is left-closed, right-infinite, and indicates Std.Rci:

term ::= ...
    | `a...*` is the range of elements greater than or equal to `a`\. See also `Std.Rci`\. term...*

This range is left-open, right-open, and indicates Std.Roo:

term ::= ...
    | `a<...b` is the range of elements greater than `a` and less than `b`\.
See also `Std.Roo`\.
term<...term

This range is left-open, right-open, and indicates Std.Roo:

term ::= ...
    | `a<...<b` is the range of elements greater than `a` and less than `b`\.
See also `Std.Roo`\.
term<...<term

This range is left-open, right-closed, and indicates Std.Roc:

term ::= ...
    | `a<...=b` is the range of elements greater than `a` and less than or equal to `b`\.
See also `Std.Roc`\.
term<...=term

This range is left-open, right-infinite, and indicates Std.Roi:

term ::= ...
    | `a<...*` is the range of elements greater than `a`\. See also `Std.Roi`\. term<...*

This range is left-infinite, right-open, and indicates Std.Rio:

term ::= ...
    | `*...b` is the range of elements less than `b`\. See also `Std.Rio`\. *...term

This range is left-infinite, right-open, and indicates Std.Ric:

term ::= ...
    | `*...<b` is the range of elements less than `b`\. See also `Std.Rio`\. *...<term

This range is left-infinite, right-closed, and indicates Std.Ric:

term ::= ...
    | `*...=b` is the range of elements less than or equal to `b`\. See also `Std.Ric`\. *...=term

This range is infinite on both sides, and indicates Std.Rii:

term ::= ...
    | `*...*` is the range that is unbounded in both directions\. See also `Std.Rii`\. *...*

20.18.1. Range Types

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

A range of elements of α with a closed lower bound and an open upper bound.

a...b or a...<b is the range of all values greater than or equal to a : α and less than b : α. This is notation for Rco.mk a b.

Constructor

Std.Rco.mk.{u}

Fields

lower : α

The lower bound of the range. lower is included in the range.

upper : α

The upper bound of the range. upper is not included in the range.

🔗def
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 α

Returns an iterator over the given range. This iterator will emit the elements of the range in increasing order.

🔗def
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 α

Returns the elements of the given left-closed right-open range as an array in ascending order.

🔗def
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 α

Returns the elements of the given left-closed right-open range as a list in ascending order.

🔗def
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

Returns the number of elements contained in the given left-closed right-open range.

🔗def
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

Checks whether the range contains any value.

This function returns a meaningful value given LawfulUpwardEnumerable and LawfulUpwardEnumerableLT instances.

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

A range of elements of α with closed lower and upper bounds.

a...=b is the range of all values greater than or equal to a : α and less than or equal to b : α. This is notation for Rcc.mk a b.

Constructor

Std.Rcc.mk.{u}

Fields

lower : α

The lower bound of the range. lower is included in the range.

upper : α

The upper bound of the range. upper is included in the range.

🔗def
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 α

Returns an iterator over the given range. This iterator will emit the elements of the range in increasing order.

🔗def
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 α

Returns the elements of the given closed range as an array in ascending order.

🔗def
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 α

Returns the elements of the given closed range as a list in ascending order.

🔗def
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

Returns the number of elements contained in the given closed range.

🔗def
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

Checks whether the range contains any value.

This function returns a meaningful value given LawfulUpwardEnumerable and LawfulUpwardEnumerableLE instances.

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

An upward-unbounded range of elements of α with a closed lower bound.

a...* is the range of all values greater than or equal to a : α. This is notation for Rci.mk a.

Constructor

Std.Rci.mk.{u}

Fields

lower : α

The lower bound of the range. lower is included in the range.

🔗def
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 α

Returns an iterator over the given range. This iterator will emit the elements of the range in increasing order.

🔗def
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 α

Returns the elements of the given left-closed right-unbounded range as an array in ascending order.

🔗def
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 α

Returns the elements of the given left-closed right-unbounded range as a list in ascending order.

🔗def
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

Returns the number of elements contained in the given left-closed right-unbounded range.

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

Checks whether the range contains any value. This function exists for completeness and always returns false: The closed lower bound is contained in the range, so left-closed right-unbounded ranges are never empty.

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

A range of elements of α with an open lower and upper bounds.

a<...b or a<...<b is the range of all values greater than a : α and less than b : α. This is notation for Roo.mk a b.

Constructor

Std.Roo.mk.{u}

Fields

lower : α

The lower bound of the range. lower is not included in the range.

upper : α

The upper bound of the range. upper is not included in the range.

🔗def
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 α

Returns an iterator over the given range. This iterator will emit the elements of the range in increasing order.

🔗def
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 α

Returns the elements of the given open range as an array in ascending order.

🔗def
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 α

Returns the elements of the given open range as a list in ascending order.

🔗def
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

Returns the number of elements contained in the given open range.

🔗def
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

Checks whether the range contains any value.

This function returns a meaningful value given LawfulUpwardEnumerable and LawfulUpwardEnumerableLT instances.

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

A range of elements of α with an open lower bound and a closed upper bound.

a<...=b is the range of all values greater than a : α and less than or equal to b : α. This is notation for Roc.mk a b.

Constructor

Std.Roc.mk.{u}

Fields

lower : α

The lower bound of the range. lower is not included in the range.

upper : α

The upper bound of the range. upper is included in the range.

🔗def
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 α

Returns an iterator over the given range. This iterator will emit the elements of the range in increasing order.

🔗def
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 α

Returns the elements of the given left-open right-closed range as an array in ascending order.

🔗def
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 α

Returns the elements of the given left-open right-closed range as a list in ascending order.

🔗def
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

Returns the number of elements contained in the given left-open right-closed range.

🔗def
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

Checks whether the range contains any value.

This function returns a meaningful value given LawfulUpwardEnumerable and LawfulUpwardEnumerableLT instances.

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

An upward-unbounded range of elements of α with an open lower bound.

a<...* is the range of all values greater than a : α. This is notation for Roi.mk a.

Constructor

Std.Roi.mk.{u}

Fields

lower : α

The lower bound of the range. lower is not included in the range.

🔗def
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 α

Returns an iterator over the given range. This iterator will emit the elements of the range in increasing order.

🔗def
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 α

Returns the elements of the given left-open right-unbounded range as an array in ascending order.

🔗def
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 α

Returns the elements of the given left-open right-unbounded range as a list in ascending order.

🔗def
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

Returns the number of elements contained in the given left-open right-unbounded range.

🔗def
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

Checks whether the range contains any value.

This function returns a meaningful value given a LawfulUpwardEnumerable instance.

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

A downward-unbounded range of elements of α with an open upper bound.

*...b or *...<b is the range of all values less than b : α. This is notation for Rio.mk b.

Constructor

Std.Rio.mk.{u}

Fields

upper : α

The upper bound of the range. upper is not included in the range.

🔗def
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 α

Returns an iterator over the given range. This iterator will emit the elements of the range in increasing order.

🔗def
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 α

Returns the elements of the given closed range as an array in ascending order.

🔗def
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 α

Returns the elements of the given closed range as a list in ascending order.

🔗def
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

Returns the number of elements contained in the given closed range.

🔗def
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

Checks whether the range contains any value.

This function returns a meaningful value given LawfulUpwardEnumerable, LawfulUpwardEnumerableLT and LawfulUpwardEnumerableLeast? instances.

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

A downward-unbounded range of elements of α with a closed upper bound.

*...=b is the range of all values less than or equal to b : α. This is notation for Ric.mk b.

Constructor

Std.Ric.mk.{u}

Fields

upper : α

The upper bound of the range. upper is included in the range.

🔗def
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 α

Returns an iterator over the given range. This iterator will emit the elements of the range in increasing order.

🔗def
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 α

Returns the elements of the given closed range as an array in ascending order.

🔗def
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 α

Returns the elements of the given closed range as a list in ascending order.

🔗def
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

Returns the number of elements contained in the given closed range.

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

Checks whether the range contains any value. This function exists for completeness and always returns false: The closed upper bound is contained in the range, so left-unbounded right-closed ranges are never empty.

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

A full range of all elements of α. Its only inhabitant is the range *...*, which is notation for Rii.mk.

Constructor

Std.Rii.mk.{u}
🔗def
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 α

Returns an iterator over the given range. This iterator will emit the elements of the range in increasing order.

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

Returns the elements of the given full range as an array in ascending order.

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

Returns the elements of the given full range as a list in ascending order.

🔗def
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

Returns the number of elements contained in the full range.

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

Checks whether the range contains any value.

This function returns a meaningful value given LawfulUpwardEnumerable and LawfulUpwardEnumerableLeast? instances.

20.18.2. Range-Related Type Classes

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

This typeclass provides the function succ? : α → Option α that computes the successor of elements of α, or none if no successor exists. It also provides the function succMany?, which computes n-th successors.

succ? is expected to be acyclic: No element is its own transitive successor. If α is ordered, then every element larger than a : α should be a transitive successor of a. These properties and the compatibility of succ? with succMany? are encoded in the typeclasses LawfulUpwardEnumerable, LawfulUpwardEnumerableLE and LawfulUpwardEnumerableLT.

Instance Constructor

Std.PRange.UpwardEnumerable.mk.{u}

Methods

succ? : α → Option α

Maps elements of α to their successor, or none if no successor exists.

succMany? : Nat → α → Option α

Maps elements of α to their n-th successor, or none if no successor exists. This should semantically behave like repeatedly applying succ?, but it might be more efficient.

LawfulUpwardEnumerable ensures the compatibility with succ?.

If no other implementation is provided in UpwardEnumerable instance, succMany? repeatedly applies succ?.

🔗def
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

According to UpwardEnumerable.LE, a is less than or equal to b if b is a or a transitive successor of a.

🔗def
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

According to UpwardEnumerable.LT, a is less than b if b is a proper transitive successor of a. 'Proper' means that b is the n-th successor of a, where n > 0.

Given LawfulUpwardEnumerable α, no element of α is less than itself.

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

This typeclass ensures that an UpwardEnumerable α instance is well-behaved.

Instance Constructor

Std.PRange.LawfulUpwardEnumerable.mk.{u}

Methods

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

There is no cyclic chain of successors.

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

The 0-th successor of a is a itself.

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

The n + 1-th successor of a is the successor of the n-th successor, given that said successors actually exist.

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

The typeclass Least? α optionally provides a smallest element of α, least? : Option α.

The main use case of this typeclass is to use it in combination with UpwardEnumerable to obtain a (possibly infinite) ascending enumeration of all elements of α.

Instance Constructor

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

Methods

least? : Option α

Returns the smallest element of α, or none if α is empty.

Only empty types are allowed to define least? := none. If α is ordered and nonempty, then the value of least? should be the smallest element according to the order on α.

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

This propositional typeclass ensures that UpwardEnumerable.succ? will never return none. In other words, it ensures that there will always be a successor.

Instance Constructor

Std.PRange.InfinitelyUpwardEnumerable.mk.{u}

Methods

isSome_succ? : ∀ (a : α), (Std.PRange.succ? a).isSome = true
🔗type class
Std.PRange.LinearlyUpwardEnumerable.{u} (α : Type u)
  [Std.PRange.UpwardEnumerable α] : Prop
Std.PRange.LinearlyUpwardEnumerable.{u}
  (α : Type u)
  [Std.PRange.UpwardEnumerable α] : Prop

This propositional typeclass ensures that UpwardEnumerable.succ? is injective.

Instance Constructor

Std.PRange.LinearlyUpwardEnumerable.mk.{u}

Methods

eq_of_succ?_eq : ∀ (a b : α), Std.PRange.succ? a = Std.PRange.succ? b → a = b
🔗type class
Std.Rxi.IsAlwaysFinite.{u} (α : Type u)
  [Std.PRange.UpwardEnumerable α] : Prop
Std.Rxi.IsAlwaysFinite.{u} (α : Type u)
  [Std.PRange.UpwardEnumerable α] : Prop

This type class ensures that right-unbounded ranges (i.e., for a bound a, a...*, a<...* and *...*) are always finite. This is a prerequisite for many functions and instances, such as Rci.toList or ForIn'.

Instance Constructor

Std.Rxi.IsAlwaysFinite.mk.{u}

Methods

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

For every elements init, there exists a chain of successors that results in an element that has no successors.

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

This typeclass provides support for the size function for ranges with closed lower bound (Ric.size, Rio.size and Rii.size).

The returned size should be equal to the number of elements returned by toList. This condition is captured by the typeclass LawfulHasSize.

Instance Constructor

Std.Rxi.HasSize.mk.{u}

Methods

size : α → Nat

Returns the number of elements starting from lo that satisfy the given upper bound.

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

This type class ensures that right-closed ranges (i.e., for bounds a and b, a...=b, a<...=b and *...=b) are always finite. This is a prerequisite for many functions and instances, such as Rcc.toList or ForIn'.

Instance Constructor

Std.Rxc.IsAlwaysFinite.mk.{u}

Methods

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

For every pair of elements init and hi, there exists a chain of successors that results in an element that either has no successors or is greater than hi.

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

This typeclass provides support for the size function for ranges with closed lower bound (Rcc.size, Rco.size and Rci.size).

The returned size should be equal to the number of elements returned by toList. This condition is captured by the typeclass LawfulHasSize.

Instance Constructor

Std.Rxc.HasSize.mk.{u}

Methods

size : α → α → Nat

Returns the number of elements starting from lo that satisfy the given upper bound.

20.18.3. Implementing Ranges

The built-in range types may be used with any type, but their usefulness depends on the presence of certain type class instances. Generally speaking, ranges are either checked for membership, enumerated or iterated over. To check whether an value is contained in a range, DecidableLT and DecidableLE instances are used to compare the value to the range's respective open and closed endpoints. To get an iterator for a range, instances of Std.PRange.UpwardEnumerable and Std.PRange.LawfulUpwardEnumerable are all that's needed. To iterate directly over it in a Lean.Parser.Term.doFor : doElem`for x in e do s` iterates over `e` assuming `e`'s type has an instance of the `ForIn` typeclass. `break` and `continue` are supported inside `for` loops. `for x in e, x2 in e2, ... do s` iterates of the given collections in parallel, until at least one of them is exhausted. The types of `e2` etc. must implement the `Std.ToStream` typeclass. for loop, Std.PRange.LawfulUpwardEnumerableLE and Std.PRange.LawfulUpwardEnumerableLT are required as well. To enumerate a range (e.g. by calling toList), it must be proven finite. This is done by supplying instances of Std.Rxi.IsAlwaysFinite, Std.Rxc.IsAlwaysFinite, or Std.Rxo.IsAlwaysFinite.

Implementing Ranges

The enumeration type Day represents the days of the week:

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

While it's already possible to use this type in ranges, they're not particularly useful. There's no membership instance:

#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.

Ranges can't be iterated over:

#eval show IO Unit from failed to synthesize instance for 'for_in%' notation ForIn (EIO IO.Error) (Std.Rcc Day) ?m.11for d in Day.mo...=Day.fr do IO.println s!"It's {repr d}" 
failed to synthesize instance for 'for_in%' notation
  ForIn (EIO IO.Error) (Std.Rcc Day) ?m.11

Nor can they be enumerated, even though the type is finite:

#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.

Membership tests require DecidableLT and DecidableLE instances. An easy way to get these is to number each day, and compare the numbers:

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))

With these instances available, membership tests work as expected:

def Day.isWeekday (d : Day) : Bool := d ∈ Day.mo...Day.sa true#eval Day.th.isWeekday 
true
false#eval Day.sa.isWeekday 
false

Iteration and enumeration are both variants on repeatedly applying a successor function until either the upper bound of the range or the largest element of the type is reached. This successor function is Std.PRange.UpwardEnumerable.succ?. It's also convenient to have a definition of the function in Day's namespace for use with generalized field notation:

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?

Iteration also requires a proof that the implementation of succ? is sensible. Its properties are expressed in terms of Std.PRange.UpwardEnumerable.succMany?, which iterates the application of succ? a certain number of times and has a default implementation in terms of Nat.repeat and succ?. In particular, an instance of LawfulUpwardEnumerable requires proofs that Std.PRange.UpwardEnumerable.succMany? corresponds to the default implementation along with a proof that repeatedly applying the successor never yields the same element again.

The first step is to write two helper lemmas for the two proofs about succMany?. While they could be written inline in the instance declaration, it's convenient for them to have the @[simp] attribute.

@[simp] theorem Day.succMany?_zero (d : Day) : Std.PRange.succMany? 0 d = some d := d:Day⊢ Std.PRange.succMany? 0 d = some d 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? := n:Natd:Day⊢ Std.PRange.succMany? (n + 1) d = (Std.PRange.succMany? n d).bind Std.PRange.succ? All goals completed! 🐙

Proving that there are no cycles in successor uses a convenient helper lemma that calculates the number of successor steps between any two days. It is marked @[grind →] because when assumptions that match its premises are present, it adds a great deal of new information:

@[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 := d:Dayd':Daysteps:Nat⊢ Std.PRange.succMany? steps d = some d' → if d ≤ d' then steps = d'.toNat - d.toNat else False d:Dayd':Daysteps:Nath:Std.PRange.succMany? steps d = some d'⊢ if d ≤ d' then steps = d'.toNat - d.toNat else False match steps with 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 d':Daysteps:Nath:Std.PRange.succMany? 6 mo = some d'⊢ if mo ≤ d' then 6 = d'.toNat - mo.toNat else Falsed':Daysteps:Nath:Std.PRange.succMany? 6 tu = some d'⊢ if tu ≤ d' then 6 = d'.toNat - tu.toNat else Falsed':Daysteps:Nath:Std.PRange.succMany? 6 we = some d'⊢ if we ≤ d' then 6 = d'.toNat - we.toNat else Falsed':Daysteps:Nath:Std.PRange.succMany? 6 th = some d'⊢ if th ≤ d' then 6 = d'.toNat - th.toNat else Falsed':Daysteps:Nath:Std.PRange.succMany? 6 fr = some d'⊢ if fr ≤ d' then 6 = d'.toNat - fr.toNat else Falsed':Daysteps:Nath:Std.PRange.succMany? 6 sa = some d'⊢ if sa ≤ d' then 6 = d'.toNat - sa.toNat else Falsed':Daysteps:Nath:Std.PRange.succMany? 6 su = some d'⊢ if su ≤ d' then 6 = d'.toNat - su.toNat else False d':Daysteps:Nath:Std.PRange.succMany? 6 mo = some d'⊢ if mo ≤ d' then 6 = d'.toNat - mo.toNat else Falsed':Daysteps:Nath:Std.PRange.succMany? 6 tu = some d'⊢ if tu ≤ d' then 6 = d'.toNat - tu.toNat else Falsed':Daysteps:Nath:Std.PRange.succMany? 6 we = some d'⊢ if we ≤ d' then 6 = d'.toNat - we.toNat else Falsed':Daysteps:Nath:Std.PRange.succMany? 6 th = some d'⊢ if th ≤ d' then 6 = d'.toNat - th.toNat else Falsed':Daysteps:Nath:Std.PRange.succMany? 6 fr = some d'⊢ if fr ≤ d' then 6 = d'.toNat - fr.toNat else Falsed':Daysteps:Nath:Std.PRange.succMany? 6 sa = some d'⊢ if sa ≤ d' then 6 = d'.toNat - sa.toNat else Falsed':Daysteps:Nath:Std.PRange.succMany? 6 su = some d'⊢ if su ≤ d' then 6 = d'.toNat - su.toNat else False steps:Nath:Std.PRange.succMany? 6 su = some mo⊢ if su ≤ mo then 6 = mo.toNat - su.toNat else Falsesteps:Nath:Std.PRange.succMany? 6 su = some tu⊢ if su ≤ tu then 6 = tu.toNat - su.toNat else Falsesteps:Nath:Std.PRange.succMany? 6 su = some we⊢ if su ≤ we then 6 = we.toNat - su.toNat else Falsesteps:Nath:Std.PRange.succMany? 6 su = some th⊢ if su ≤ th then 6 = th.toNat - su.toNat else Falsesteps:Nath:Std.PRange.succMany? 6 su = some fr⊢ if su ≤ fr then 6 = fr.toNat - su.toNat else Falsesteps:Nath:Std.PRange.succMany? 6 su = some sa⊢ if su ≤ sa then 6 = sa.toNat - su.toNat else Falsesteps:Nath:Std.PRange.succMany? 6 su = some su⊢ if su ≤ su then 6 = su.toNat - su.toNat else False steps:Nath:Std.PRange.succMany? 6 mo = some mo⊢ if mo ≤ mo then 6 = mo.toNat - mo.toNat else Falsesteps:Nath:Std.PRange.succMany? 6 mo = some tu⊢ if mo ≤ tu then 6 = tu.toNat - mo.toNat else Falsesteps:Nath:Std.PRange.succMany? 6 mo = some we⊢ if mo ≤ we then 6 = we.toNat - mo.toNat else Falsesteps:Nath:Std.PRange.succMany? 6 mo = some th⊢ if mo ≤ th then 6 = th.toNat - mo.toNat else Falsesteps:Nath:Std.PRange.succMany? 6 mo = some fr⊢ if mo ≤ fr then 6 = fr.toNat - mo.toNat else Falsesteps:Nath:Std.PRange.succMany? 6 mo = some sa⊢ if mo ≤ sa then 6 = sa.toNat - mo.toNat else Falsesteps:Nath:Std.PRange.succMany? 6 mo = some su⊢ if mo ≤ su then 6 = su.toNat - mo.toNat else Falsesteps:Nath:Std.PRange.succMany? 6 tu = some mo⊢ if tu ≤ mo then 6 = mo.toNat - tu.toNat else Falsesteps:Nath:Std.PRange.succMany? 6 tu = some tu⊢ if tu ≤ tu then 6 = tu.toNat - tu.toNat else Falsesteps:Nath:Std.PRange.succMany? 6 tu = some we⊢ if tu ≤ we then 6 = we.toNat - tu.toNat else Falsesteps:Nath:Std.PRange.succMany? 6 tu = some th⊢ if tu ≤ th then 6 = th.toNat - tu.toNat else Falsesteps:Nath:Std.PRange.succMany? 6 tu = some fr⊢ if tu ≤ fr then 6 = fr.toNat - tu.toNat else Falsesteps:Nath:Std.PRange.succMany? 6 tu = some sa⊢ if tu ≤ sa then 6 = sa.toNat - tu.toNat else Falsesteps:Nath:Std.PRange.succMany? 6 tu = some su⊢ if tu ≤ su then 6 = su.toNat - tu.toNat else Falsesteps:Nath:Std.PRange.succMany? 6 we = some mo⊢ if we ≤ mo then 6 = mo.toNat - we.toNat else Falsesteps:Nath:Std.PRange.succMany? 6 we = some tu⊢ if we ≤ tu then 6 = tu.toNat - we.toNat else Falsesteps:Nath:Std.PRange.succMany? 6 we = some we⊢ if we ≤ we then 6 = we.toNat - we.toNat else Falsesteps:Nath:Std.PRange.succMany? 6 we = some th⊢ if we ≤ th then 6 = th.toNat - we.toNat else Falsesteps:Nath:Std.PRange.succMany? 6 we = some fr⊢ if we ≤ fr then 6 = fr.toNat - we.toNat else Falsesteps:Nath:Std.PRange.succMany? 6 we = some sa⊢ if we ≤ sa then 6 = sa.toNat - we.toNat else Falsesteps:Nath:Std.PRange.succMany? 6 we = some su⊢ if we ≤ su then 6 = su.toNat - we.toNat else Falsesteps:Nath:Std.PRange.succMany? 6 th = some mo⊢ if th ≤ mo then 6 = mo.toNat - th.toNat else Falsesteps:Nath:Std.PRange.succMany? 6 th = some tu⊢ if th ≤ tu then 6 = tu.toNat - th.toNat else Falsesteps:Nath:Std.PRange.succMany? 6 th = some we⊢ if th ≤ we then 6 = we.toNat - th.toNat else Falsesteps:Nath:Std.PRange.succMany? 6 th = some th⊢ if th ≤ th then 6 = th.toNat - th.toNat else Falsesteps:Nath:Std.PRange.succMany? 6 th = some fr⊢ if th ≤ fr then 6 = fr.toNat - th.toNat else Falsesteps:Nath:Std.PRange.succMany? 6 th = some sa⊢ if th ≤ sa then 6 = sa.toNat - th.toNat else Falsesteps:Nath:Std.PRange.succMany? 6 th = some su⊢ if th ≤ su then 6 = su.toNat - th.toNat else Falsesteps:Nath:Std.PRange.succMany? 6 fr = some mo⊢ if fr ≤ mo then 6 = mo.toNat - fr.toNat else Falsesteps:Nath:Std.PRange.succMany? 6 fr = some tu⊢ if fr ≤ tu then 6 = tu.toNat - fr.toNat else Falsesteps:Nath:Std.PRange.succMany? 6 fr = some we⊢ if fr ≤ we then 6 = we.toNat - fr.toNat else Falsesteps:Nath:Std.PRange.succMany? 6 fr = some th⊢ if fr ≤ th then 6 = th.toNat - fr.toNat else Falsesteps:Nath:Std.PRange.succMany? 6 fr = some fr⊢ if fr ≤ fr then 6 = fr.toNat - fr.toNat else Falsesteps:Nath:Std.PRange.succMany? 6 fr = some sa⊢ if fr ≤ sa then 6 = sa.toNat - fr.toNat else Falsesteps:Nath:Std.PRange.succMany? 6 fr = some su⊢ if fr ≤ su then 6 = su.toNat - fr.toNat else Falsesteps:Nath:Std.PRange.succMany? 6 sa = some mo⊢ if sa ≤ mo then 6 = mo.toNat - sa.toNat else Falsesteps:Nath:Std.PRange.succMany? 6 sa = some tu⊢ if sa ≤ tu then 6 = tu.toNat - sa.toNat else Falsesteps:Nath:Std.PRange.succMany? 6 sa = some we⊢ if sa ≤ we then 6 = we.toNat - sa.toNat else Falsesteps:Nath:Std.PRange.succMany? 6 sa = some th⊢ if sa ≤ th then 6 = th.toNat - sa.toNat else Falsesteps:Nath:Std.PRange.succMany? 6 sa = some fr⊢ if sa ≤ fr then 6 = fr.toNat - sa.toNat else Falsesteps:Nath:Std.PRange.succMany? 6 sa = some sa⊢ if sa ≤ sa then 6 = sa.toNat - sa.toNat else Falsesteps:Nath:Std.PRange.succMany? 6 sa = some su⊢ if sa ≤ su then 6 = su.toNat - sa.toNat else Falsesteps:Nath:Std.PRange.succMany? 6 su = some mo⊢ if su ≤ mo then 6 = mo.toNat - su.toNat else Falsesteps:Nath:Std.PRange.succMany? 6 su = some tu⊢ if su ≤ tu then 6 = tu.toNat - su.toNat else Falsesteps:Nath:Std.PRange.succMany? 6 su = some we⊢ if su ≤ we then 6 = we.toNat - su.toNat else Falsesteps:Nath:Std.PRange.succMany? 6 su = some th⊢ if su ≤ th then 6 = th.toNat - su.toNat else Falsesteps:Nath:Std.PRange.succMany? 6 su = some fr⊢ if su ≤ fr then 6 = fr.toNat - su.toNat else Falsesteps:Nath:Std.PRange.succMany? 6 su = some sa⊢ if su ≤ sa then 6 = sa.toNat - su.toNat else Falsesteps:Nath:Std.PRange.succMany? 6 su = some su⊢ if su ≤ su then 6 = su.toNat - su.toNat else False All goals completed! 🐙 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 d: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 d: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 All goals completed! 🐙 d: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 d: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 d: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 Falsed: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 Falsed: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 Falsed: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 Falsed: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 Falsed: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 Falsed: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 d: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 Falsed: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 Falsed: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 Falsed: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 Falsed: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 Falsed: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 Falsed: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 All goals completed! 🐙

With that helper, the proof is quite short:

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

Proving the three kinds of enumerable ranges to be finite makes it possible to enumerate ranges of days:

instance : Std.Rxo.IsAlwaysFinite Day where finite init hi := ⟨7, init:Dayhi:Day⊢ (Std.PRange.succMany? 7 init).elim True fun x => ¬x < hi hi:Day⊢ (Std.PRange.succMany? 7 Day.mo).elim True fun x => ¬x < hihi:Day⊢ (Std.PRange.succMany? 7 Day.tu).elim True fun x => ¬x < hihi:Day⊢ (Std.PRange.succMany? 7 Day.we).elim True fun x => ¬x < hihi:Day⊢ (Std.PRange.succMany? 7 Day.th).elim True fun x => ¬x < hihi:Day⊢ (Std.PRange.succMany? 7 Day.fr).elim True fun x => ¬x < hihi:Day⊢ (Std.PRange.succMany? 7 Day.sa).elim True fun x => ¬x < hihi:Day⊢ (Std.PRange.succMany? 7 Day.su).elim True fun x => ¬x < hi hi:Day⊢ (Std.PRange.succMany? 7 Day.mo).elim True fun x => ¬x < hihi:Day⊢ (Std.PRange.succMany? 7 Day.tu).elim True fun x => ¬x < hihi:Day⊢ (Std.PRange.succMany? 7 Day.we).elim True fun x => ¬x < hihi:Day⊢ (Std.PRange.succMany? 7 Day.th).elim True fun x => ¬x < hihi:Day⊢ (Std.PRange.succMany? 7 Day.fr).elim True fun x => ¬x < hihi:Day⊢ (Std.PRange.succMany? 7 Day.sa).elim True fun x => ¬x < hihi:Day⊢ (Std.PRange.succMany? 7 Day.su).elim True fun x => ¬x < hi All goals completed! 🐙⟩ instance : Std.Rxc.IsAlwaysFinite Day where finite init hi := ⟨7, init:Dayhi:Day⊢ (Std.PRange.succMany? 7 init).elim True fun x => ¬x ≤ hi hi:Day⊢ (Std.PRange.succMany? 7 Day.mo).elim True fun x => ¬x ≤ hihi:Day⊢ (Std.PRange.succMany? 7 Day.tu).elim True fun x => ¬x ≤ hihi:Day⊢ (Std.PRange.succMany? 7 Day.we).elim True fun x => ¬x ≤ hihi:Day⊢ (Std.PRange.succMany? 7 Day.th).elim True fun x => ¬x ≤ hihi:Day⊢ (Std.PRange.succMany? 7 Day.fr).elim True fun x => ¬x ≤ hihi:Day⊢ (Std.PRange.succMany? 7 Day.sa).elim True fun x => ¬x ≤ hihi:Day⊢ (Std.PRange.succMany? 7 Day.su).elim True fun x => ¬x ≤ hi hi:Day⊢ (Std.PRange.succMany? 7 Day.mo).elim True fun x => ¬x ≤ hihi:Day⊢ (Std.PRange.succMany? 7 Day.tu).elim True fun x => ¬x ≤ hihi:Day⊢ (Std.PRange.succMany? 7 Day.we).elim True fun x => ¬x ≤ hihi:Day⊢ (Std.PRange.succMany? 7 Day.th).elim True fun x => ¬x ≤ hihi:Day⊢ (Std.PRange.succMany? 7 Day.fr).elim True fun x => ¬x ≤ hihi:Day⊢ (Std.PRange.succMany? 7 Day.sa).elim True fun x => ¬x ≤ hihi:Day⊢ (Std.PRange.succMany? 7 Day.su).elim True fun x => ¬x ≤ hi All goals completed! 🐙⟩ instance : Std.Rxi.IsAlwaysFinite Day where finite init := ⟨7, init:Day⊢ Std.PRange.succMany? 7 init = none ⊢ Std.PRange.succMany? 7 Day.mo = none⊢ Std.PRange.succMany? 7 Day.tu = none⊢ Std.PRange.succMany? 7 Day.we = none⊢ Std.PRange.succMany? 7 Day.th = none⊢ Std.PRange.succMany? 7 Day.fr = none⊢ Std.PRange.succMany? 7 Day.sa = none⊢ Std.PRange.succMany? 7 Day.su = none ⊢ Std.PRange.succMany? 7 Day.mo = none⊢ Std.PRange.succMany? 7 Day.tu = none⊢ Std.PRange.succMany? 7 Day.we = none⊢ Std.PRange.succMany? 7 Day.th = none⊢ Std.PRange.succMany? 7 Day.fr = none⊢ Std.PRange.succMany? 7 Day.sa = none⊢ Std.PRange.succMany? 7 Day.su = none All 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]

Adding a Std.PRange.Least? instance allows enumeration of left-unbounded ranges:

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]

It's also possible to create an iterator that can be enumerated, but it can't yet be used with Lean.Parser.Term.doFor : doElem`for x in e do s` iterates over `e` assuming `e`'s type has an instance of the `ForIn` typeclass. `break` and `continue` are supported inside `for` loops. `for x in e, x2 in e2, ... do s` iterates of the given collections in parallel, until at least one of them is exhausted. The types of `e2` etc. must implement the `Std.ToStream` typeclass. for:

[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 for 'for_in%' notation ForIn (EIO IO.Error) (Std.Iter Day) ?m.12for d in (Day.mo...Day.th).iter do IO.println s!"It's {repr d}." 
failed to synthesize instance for 'for_in%' notation
  ForIn (EIO IO.Error) (Std.Iter Day) ?m.12

The last step to enable iteration, thus making ranges of days fully-featured, is to prove that the less-than and less-than-or-equal-to relations on Day correspond to the notions of inequality that are derived from iterating the successor function. This is captured in the classes Std.PRange.LawfulUpwardEnumerableLT and Std.PRange.LawfulUpwardEnumerableLE, which require that the two notions are logically equivalent:

instance : Std.PRange.LawfulUpwardEnumerableLT Day where lt_iff d1 d2 := d1:Dayd2:Day⊢ d1 < d2 ↔ Std.PRange.UpwardEnumerable.LT d1 d2 d1:Dayd2:Day⊢ d1 < d2 → Std.PRange.UpwardEnumerable.LT d1 d2d1:Dayd2:Day⊢ Std.PRange.UpwardEnumerable.LT d1 d2 → d1 < d2 d1:Dayd2:Day⊢ d1 < d2 → Std.PRange.UpwardEnumerable.LT d1 d2 d1:Dayd2:Daylt:d1 < d2⊢ Std.PRange.UpwardEnumerable.LT d1 d2 d1:Dayd2:Daylt:d1 < d2⊢ ∃ n, (Std.PRange.succMany? n d1).bind Std.PRange.succ? = some d2 d1:Dayd2:Daylt:d1 < d2⊢ (Std.PRange.succMany? (d2.toNat - d1.toNat.succ) d1).bind Std.PRange.succ? = some d2 d2:Daylt:Day.mo < d2⊢ (Std.PRange.succMany? (d2.toNat - Day.mo.toNat.succ) Day.mo).bind Std.PRange.succ? = some d2d2:Daylt:Day.tu < d2⊢ (Std.PRange.succMany? (d2.toNat - Day.tu.toNat.succ) Day.tu).bind Std.PRange.succ? = some d2d2:Daylt:Day.we < d2⊢ (Std.PRange.succMany? (d2.toNat - Day.we.toNat.succ) Day.we).bind Std.PRange.succ? = some d2d2:Daylt:Day.th < d2⊢ (Std.PRange.succMany? (d2.toNat - Day.th.toNat.succ) Day.th).bind Std.PRange.succ? = some d2d2:Daylt:Day.fr < d2⊢ (Std.PRange.succMany? (d2.toNat - Day.fr.toNat.succ) Day.fr).bind Std.PRange.succ? = some d2d2:Daylt:Day.sa < d2⊢ (Std.PRange.succMany? (d2.toNat - Day.sa.toNat.succ) Day.sa).bind Std.PRange.succ? = some d2d2:Daylt:Day.su < d2⊢ (Std.PRange.succMany? (d2.toNat - Day.su.toNat.succ) Day.su).bind Std.PRange.succ? = some d2 d2:Daylt:Day.mo < d2⊢ (Std.PRange.succMany? (d2.toNat - Day.mo.toNat.succ) Day.mo).bind Std.PRange.succ? = some d2d2:Daylt:Day.tu < d2⊢ (Std.PRange.succMany? (d2.toNat - Day.tu.toNat.succ) Day.tu).bind Std.PRange.succ? = some d2d2:Daylt:Day.we < d2⊢ (Std.PRange.succMany? (d2.toNat - Day.we.toNat.succ) Day.we).bind Std.PRange.succ? = some d2d2:Daylt:Day.th < d2⊢ (Std.PRange.succMany? (d2.toNat - Day.th.toNat.succ) Day.th).bind Std.PRange.succ? = some d2d2:Daylt:Day.fr < d2⊢ (Std.PRange.succMany? (d2.toNat - Day.fr.toNat.succ) Day.fr).bind Std.PRange.succ? = some d2d2:Daylt:Day.sa < d2⊢ (Std.PRange.succMany? (d2.toNat - Day.sa.toNat.succ) Day.sa).bind Std.PRange.succ? = some d2d2:Daylt:Day.su < d2⊢ (Std.PRange.succMany? (d2.toNat - Day.su.toNat.succ) Day.su).bind Std.PRange.succ? = some d2 lt:Day.su < Day.mo⊢ (Std.PRange.succMany? (Day.mo.toNat - Day.su.toNat.succ) Day.su).bind Std.PRange.succ? = some Day.molt:Day.su < Day.tu⊢ (Std.PRange.succMany? (Day.tu.toNat - Day.su.toNat.succ) Day.su).bind Std.PRange.succ? = some Day.tult:Day.su < Day.we⊢ (Std.PRange.succMany? (Day.we.toNat - Day.su.toNat.succ) Day.su).bind Std.PRange.succ? = some Day.welt:Day.su < Day.th⊢ (Std.PRange.succMany? (Day.th.toNat - Day.su.toNat.succ) Day.su).bind Std.PRange.succ? = some Day.thlt:Day.su < Day.fr⊢ (Std.PRange.succMany? (Day.fr.toNat - Day.su.toNat.succ) Day.su).bind Std.PRange.succ? = some Day.frlt:Day.su < Day.sa⊢ (Std.PRange.succMany? (Day.sa.toNat - Day.su.toNat.succ) Day.su).bind Std.PRange.succ? = some Day.salt:Day.su < Day.su⊢ (Std.PRange.succMany? (Day.su.toNat - Day.su.toNat.succ) Day.su).bind Std.PRange.succ? = some Day.su lt:Day.mo < Day.mo⊢ (Std.PRange.succMany? (Day.mo.toNat - Day.mo.toNat.succ) Day.mo).bind Std.PRange.succ? = some Day.molt:Day.mo < Day.tu⊢ (Std.PRange.succMany? (Day.tu.toNat - Day.mo.toNat.succ) Day.mo).bind Std.PRange.succ? = some Day.tult:Day.mo < Day.we⊢ (Std.PRange.succMany? (Day.we.toNat - Day.mo.toNat.succ) Day.mo).bind Std.PRange.succ? = some Day.welt:Day.mo < Day.th⊢ (Std.PRange.succMany? (Day.th.toNat - Day.mo.toNat.succ) Day.mo).bind Std.PRange.succ? = some Day.thlt:Day.mo < Day.fr⊢ (Std.PRange.succMany? (Day.fr.toNat - Day.mo.toNat.succ) Day.mo).bind Std.PRange.succ? = some Day.frlt:Day.mo < Day.sa⊢ (Std.PRange.succMany? (Day.sa.toNat - Day.mo.toNat.succ) Day.mo).bind Std.PRange.succ? = some Day.salt:Day.mo < Day.su⊢ (Std.PRange.succMany? (Day.su.toNat - Day.mo.toNat.succ) Day.mo).bind Std.PRange.succ? = some Day.sult:Day.tu < Day.mo⊢ (Std.PRange.succMany? (Day.mo.toNat - Day.tu.toNat.succ) Day.tu).bind Std.PRange.succ? = some Day.molt:Day.tu < Day.tu⊢ (Std.PRange.succMany? (Day.tu.toNat - Day.tu.toNat.succ) Day.tu).bind Std.PRange.succ? = some Day.tult:Day.tu < Day.we⊢ (Std.PRange.succMany? (Day.we.toNat - Day.tu.toNat.succ) Day.tu).bind Std.PRange.succ? = some Day.welt:Day.tu < Day.th⊢ (Std.PRange.succMany? (Day.th.toNat - Day.tu.toNat.succ) Day.tu).bind Std.PRange.succ? = some Day.thlt:Day.tu < Day.fr⊢ (Std.PRange.succMany? (Day.fr.toNat - Day.tu.toNat.succ) Day.tu).bind Std.PRange.succ? = some Day.frlt:Day.tu < Day.sa⊢ (Std.PRange.succMany? (Day.sa.toNat - Day.tu.toNat.succ) Day.tu).bind Std.PRange.succ? = some Day.salt:Day.tu < Day.su⊢ (Std.PRange.succMany? (Day.su.toNat - Day.tu.toNat.succ) Day.tu).bind Std.PRange.succ? = some Day.sult:Day.we < Day.mo⊢ (Std.PRange.succMany? (Day.mo.toNat - Day.we.toNat.succ) Day.we).bind Std.PRange.succ? = some Day.molt:Day.we < Day.tu⊢ (Std.PRange.succMany? (Day.tu.toNat - Day.we.toNat.succ) Day.we).bind Std.PRange.succ? = some Day.tult:Day.we < Day.we⊢ (Std.PRange.succMany? (Day.we.toNat - Day.we.toNat.succ) Day.we).bind Std.PRange.succ? = some Day.welt:Day.we < Day.th⊢ (Std.PRange.succMany? (Day.th.toNat - Day.we.toNat.succ) Day.we).bind Std.PRange.succ? = some Day.thlt:Day.we < Day.fr⊢ (Std.PRange.succMany? (Day.fr.toNat - Day.we.toNat.succ) Day.we).bind Std.PRange.succ? = some Day.frlt:Day.we < Day.sa⊢ (Std.PRange.succMany? (Day.sa.toNat - Day.we.toNat.succ) Day.we).bind Std.PRange.succ? = some Day.salt:Day.we < Day.su⊢ (Std.PRange.succMany? (Day.su.toNat - Day.we.toNat.succ) Day.we).bind Std.PRange.succ? = some Day.sult:Day.th < Day.mo⊢ (Std.PRange.succMany? (Day.mo.toNat - Day.th.toNat.succ) Day.th).bind Std.PRange.succ? = some Day.molt:Day.th < Day.tu⊢ (Std.PRange.succMany? (Day.tu.toNat - Day.th.toNat.succ) Day.th).bind Std.PRange.succ? = some Day.tult:Day.th < Day.we⊢ (Std.PRange.succMany? (Day.we.toNat - Day.th.toNat.succ) Day.th).bind Std.PRange.succ? = some Day.welt:Day.th < Day.th⊢ (Std.PRange.succMany? (Day.th.toNat - Day.th.toNat.succ) Day.th).bind Std.PRange.succ? = some Day.thlt:Day.th < Day.fr⊢ (Std.PRange.succMany? (Day.fr.toNat - Day.th.toNat.succ) Day.th).bind Std.PRange.succ? = some Day.frlt:Day.th < Day.sa⊢ (Std.PRange.succMany? (Day.sa.toNat - Day.th.toNat.succ) Day.th).bind Std.PRange.succ? = some Day.salt:Day.th < Day.su⊢ (Std.PRange.succMany? (Day.su.toNat - Day.th.toNat.succ) Day.th).bind Std.PRange.succ? = some Day.sult:Day.fr < Day.mo⊢ (Std.PRange.succMany? (Day.mo.toNat - Day.fr.toNat.succ) Day.fr).bind Std.PRange.succ? = some Day.molt:Day.fr < Day.tu⊢ (Std.PRange.succMany? (Day.tu.toNat - Day.fr.toNat.succ) Day.fr).bind Std.PRange.succ? = some Day.tult:Day.fr < Day.we⊢ (Std.PRange.succMany? (Day.we.toNat - Day.fr.toNat.succ) Day.fr).bind Std.PRange.succ? = some Day.welt:Day.fr < Day.th⊢ (Std.PRange.succMany? (Day.th.toNat - Day.fr.toNat.succ) Day.fr).bind Std.PRange.succ? = some Day.thlt:Day.fr < Day.fr⊢ (Std.PRange.succMany? (Day.fr.toNat - Day.fr.toNat.succ) Day.fr).bind Std.PRange.succ? = some Day.frlt:Day.fr < Day.sa⊢ (Std.PRange.succMany? (Day.sa.toNat - Day.fr.toNat.succ) Day.fr).bind Std.PRange.succ? = some Day.salt:Day.fr < Day.su⊢ (Std.PRange.succMany? (Day.su.toNat - Day.fr.toNat.succ) Day.fr).bind Std.PRange.succ? = some Day.sult:Day.sa < Day.mo⊢ (Std.PRange.succMany? (Day.mo.toNat - Day.sa.toNat.succ) Day.sa).bind Std.PRange.succ? = some Day.molt:Day.sa < Day.tu⊢ (Std.PRange.succMany? (Day.tu.toNat - Day.sa.toNat.succ) Day.sa).bind Std.PRange.succ? = some Day.tult:Day.sa < Day.we⊢ (Std.PRange.succMany? (Day.we.toNat - Day.sa.toNat.succ) Day.sa).bind Std.PRange.succ? = some Day.welt:Day.sa < Day.th⊢ (Std.PRange.succMany? (Day.th.toNat - Day.sa.toNat.succ) Day.sa).bind Std.PRange.succ? = some Day.thlt:Day.sa < Day.fr⊢ (Std.PRange.succMany? (Day.fr.toNat - Day.sa.toNat.succ) Day.sa).bind Std.PRange.succ? = some Day.frlt:Day.sa < Day.sa⊢ (Std.PRange.succMany? (Day.sa.toNat - Day.sa.toNat.succ) Day.sa).bind Std.PRange.succ? = some Day.salt:Day.sa < Day.su⊢ (Std.PRange.succMany? (Day.su.toNat - Day.sa.toNat.succ) Day.sa).bind Std.PRange.succ? = some Day.sult:Day.su < Day.mo⊢ (Std.PRange.succMany? (Day.mo.toNat - Day.su.toNat.succ) Day.su).bind Std.PRange.succ? = some Day.molt:Day.su < Day.tu⊢ (Std.PRange.succMany? (Day.tu.toNat - Day.su.toNat.succ) Day.su).bind Std.PRange.succ? = some Day.tult:Day.su < Day.we⊢ (Std.PRange.succMany? (Day.we.toNat - Day.su.toNat.succ) Day.su).bind Std.PRange.succ? = some Day.welt:Day.su < Day.th⊢ (Std.PRange.succMany? (Day.th.toNat - Day.su.toNat.succ) Day.su).bind Std.PRange.succ? = some Day.thlt:Day.su < Day.fr⊢ (Std.PRange.succMany? (Day.fr.toNat - Day.su.toNat.succ) Day.su).bind Std.PRange.succ? = some Day.frlt:Day.su < Day.sa⊢ (Std.PRange.succMany? (Day.sa.toNat - Day.su.toNat.succ) Day.su).bind Std.PRange.succ? = some Day.salt:Day.su < Day.su⊢ (Std.PRange.succMany? (Day.su.toNat - Day.su.toNat.succ) Day.su).bind Std.PRange.succ? = some Day.su lt:Day.su < Day.su⊢ False lt:Day.mo < Day.mo⊢ Falselt:Day.tu < Day.mo⊢ Falselt:Day.tu < Day.tu⊢ Falselt:Day.we < Day.mo⊢ Falselt:Day.we < Day.tu⊢ Falselt:Day.we < Day.we⊢ Falselt:Day.th < Day.mo⊢ Falselt:Day.th < Day.tu⊢ Falselt:Day.th < Day.we⊢ Falselt:Day.th < Day.th⊢ Falselt:Day.fr < Day.mo⊢ Falselt:Day.fr < Day.tu⊢ Falselt:Day.fr < Day.we⊢ Falselt:Day.fr < Day.th⊢ Falselt:Day.fr < Day.fr⊢ Falselt:Day.sa < Day.mo⊢ Falselt:Day.sa < Day.tu⊢ Falselt:Day.sa < Day.we⊢ Falselt:Day.sa < Day.th⊢ Falselt:Day.sa < Day.fr⊢ Falselt:Day.sa < Day.sa⊢ Falselt:Day.su < Day.mo⊢ Falselt:Day.su < Day.tu⊢ Falselt:Day.su < Day.we⊢ Falselt:Day.su < Day.th⊢ Falselt:Day.su < Day.fr⊢ Falselt:Day.su < Day.sa⊢ Falselt:Day.su < Day.su⊢ False All goals completed! 🐙 d1:Dayd2:Day⊢ Std.PRange.UpwardEnumerable.LT d1 d2 → d1 < d2 d1:Dayd2:Daysteps:Nateq:Std.PRange.succMany? (steps + 1) d1 = some d2⊢ d1 < d2 d1:Dayd2:Daysteps:Nateq:Std.PRange.succMany? (steps + 1) d1 = some d2this:if d1 ≤ d2 then steps + 1 = d2.toNat - d1.toNat else False := Day.succMany?_steps eq⊢ d1 < d2 d2: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 < d2d2: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 < d2d2: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 < d2d2: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 < d2d2: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 < d2d2: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 < d2d2: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 d2: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 < d2d2: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 < d2d2: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 < d2d2: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 < d2d2: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 < d2d2: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 < d2d2: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 steps: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.mosteps: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.tusteps: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.westeps: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.thsteps: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.frsteps: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.sasteps: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 steps: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.mosteps: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.tusteps: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.westeps: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.thsteps: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.frsteps: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.sasteps: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.susteps: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.mosteps: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.tusteps: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.westeps: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.thsteps: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.frsteps: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.sasteps: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.susteps: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.mosteps: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.tusteps: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.westeps: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.thsteps: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.frsteps: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.sasteps: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.susteps: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.mosteps: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.tusteps: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.westeps: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.thsteps: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.frsteps: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.sasteps: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.susteps: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.mosteps: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.tusteps: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.westeps: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.thsteps: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.frsteps: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.sasteps: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.susteps: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.mosteps: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.tusteps: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.westeps: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.thsteps: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.frsteps: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.sasteps: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.susteps: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.mosteps: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.tusteps: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.westeps: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.thsteps: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.frsteps: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.sasteps: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 steps: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 steps: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.mosteps: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.tusteps: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.westeps: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.thsteps: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.frsteps: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.sasteps: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.susteps: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.mosteps: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.tusteps: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.westeps: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.thsteps: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.frsteps: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.sasteps: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.susteps: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.mosteps: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.tusteps: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.westeps: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.thsteps: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.frsteps: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.sasteps: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.susteps: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.mosteps: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.tusteps: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.westeps: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.thsteps: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.frsteps: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.sasteps: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.susteps: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.mosteps: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.tusteps: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.westeps: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.thsteps: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.frsteps: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.sasteps: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.susteps: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.mosteps: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.tusteps: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.westeps: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.thsteps: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.frsteps: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.sasteps: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.susteps: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.mosteps: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.tusteps: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.westeps: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.thsteps: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.frsteps: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.sasteps: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 steps: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 steps: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.mosteps: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.tusteps: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.westeps: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.thsteps: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.frsteps: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.sasteps: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.susteps: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.mosteps: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.tusteps: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.westeps: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.thsteps: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.frsteps: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.sasteps: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.susteps: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.mosteps: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.tusteps: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.westeps: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.thsteps: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.frsteps: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.sasteps: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.susteps: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.mosteps: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.tusteps: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.westeps: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.thsteps: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.frsteps: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.sasteps: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.susteps: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.mosteps: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.tusteps: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.westeps: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.thsteps: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.frsteps: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.sasteps: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.susteps: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.mosteps: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.tusteps: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.westeps: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.thsteps: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.frsteps: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.sasteps: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.susteps: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.mosteps: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.tusteps: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.westeps: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.thsteps: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.frsteps: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.sasteps: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 | steps: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 | All goals completed! 🐙 instance : Std.PRange.LawfulUpwardEnumerableLE Day where le_iff d1 d2 := d1:Dayd2:Day⊢ d1 ≤ d2 ↔ Std.PRange.UpwardEnumerable.LE d1 d2 d1:Dayd2:Day⊢ d1 ≤ d2 → Std.PRange.UpwardEnumerable.LE d1 d2d1:Dayd2:Day⊢ Std.PRange.UpwardEnumerable.LE d1 d2 → d1 ≤ d2 d1:Dayd2:Day⊢ d1 ≤ d2 → Std.PRange.UpwardEnumerable.LE d1 d2 d1:Dayd2:Dayle:d1 ≤ d2⊢ Std.PRange.UpwardEnumerable.LE d1 d2 d1:Dayd2:Dayle:d1 ≤ d2⊢ ∃ n, Std.PRange.succMany? n d1 = some d2 d1:Dayd2:Dayle:d1 ≤ d2⊢ Std.PRange.succMany? (d2.toNat - d1.toNat) d1 = some d2 d2:Dayle:Day.mo ≤ d2⊢ Std.PRange.succMany? (d2.toNat - Day.mo.toNat) Day.mo = some d2d2:Dayle:Day.tu ≤ d2⊢ Std.PRange.succMany? (d2.toNat - Day.tu.toNat) Day.tu = some d2d2:Dayle:Day.we ≤ d2⊢ Std.PRange.succMany? (d2.toNat - Day.we.toNat) Day.we = some d2d2:Dayle:Day.th ≤ d2⊢ Std.PRange.succMany? (d2.toNat - Day.th.toNat) Day.th = some d2d2:Dayle:Day.fr ≤ d2⊢ Std.PRange.succMany? (d2.toNat - Day.fr.toNat) Day.fr = some d2d2:Dayle:Day.sa ≤ d2⊢ Std.PRange.succMany? (d2.toNat - Day.sa.toNat) Day.sa = some d2d2:Dayle:Day.su ≤ d2⊢ Std.PRange.succMany? (d2.toNat - Day.su.toNat) Day.su = some d2 d2:Dayle:Day.mo ≤ d2⊢ Std.PRange.succMany? (d2.toNat - Day.mo.toNat) Day.mo = some d2d2:Dayle:Day.tu ≤ d2⊢ Std.PRange.succMany? (d2.toNat - Day.tu.toNat) Day.tu = some d2d2:Dayle:Day.we ≤ d2⊢ Std.PRange.succMany? (d2.toNat - Day.we.toNat) Day.we = some d2d2:Dayle:Day.th ≤ d2⊢ Std.PRange.succMany? (d2.toNat - Day.th.toNat) Day.th = some d2d2:Dayle:Day.fr ≤ d2⊢ Std.PRange.succMany? (d2.toNat - Day.fr.toNat) Day.fr = some d2d2:Dayle:Day.sa ≤ d2⊢ Std.PRange.succMany? (d2.toNat - Day.sa.toNat) Day.sa = some d2d2:Dayle:Day.su ≤ d2⊢ Std.PRange.succMany? (d2.toNat - Day.su.toNat) Day.su = some d2 le:Day.su ≤ Day.mo⊢ Std.PRange.succMany? (Day.mo.toNat - Day.su.toNat) Day.su = some Day.mole:Day.su ≤ Day.tu⊢ Std.PRange.succMany? (Day.tu.toNat - Day.su.toNat) Day.su = some Day.tule:Day.su ≤ Day.we⊢ Std.PRange.succMany? (Day.we.toNat - Day.su.toNat) Day.su = some Day.wele:Day.su ≤ Day.th⊢ Std.PRange.succMany? (Day.th.toNat - Day.su.toNat) Day.su = some Day.thle:Day.su ≤ Day.fr⊢ Std.PRange.succMany? (Day.fr.toNat - Day.su.toNat) Day.su = some Day.frle:Day.su ≤ Day.sa⊢ Std.PRange.succMany? (Day.sa.toNat - Day.su.toNat) Day.su = some Day.sale:Day.su ≤ Day.su⊢ Std.PRange.succMany? (Day.su.toNat - Day.su.toNat) Day.su = some Day.su le:Day.mo ≤ Day.mo⊢ Std.PRange.succMany? (Day.mo.toNat - Day.mo.toNat) Day.mo = some Day.mole:Day.mo ≤ Day.tu⊢ Std.PRange.succMany? (Day.tu.toNat - Day.mo.toNat) Day.mo = some Day.tule:Day.mo ≤ Day.we⊢ Std.PRange.succMany? (Day.we.toNat - Day.mo.toNat) Day.mo = some Day.wele:Day.mo ≤ Day.th⊢ Std.PRange.succMany? (Day.th.toNat - Day.mo.toNat) Day.mo = some Day.thle:Day.mo ≤ Day.fr⊢ Std.PRange.succMany? (Day.fr.toNat - Day.mo.toNat) Day.mo = some Day.frle:Day.mo ≤ Day.sa⊢ Std.PRange.succMany? (Day.sa.toNat - Day.mo.toNat) Day.mo = some Day.sale:Day.mo ≤ Day.su⊢ Std.PRange.succMany? (Day.su.toNat - Day.mo.toNat) Day.mo = some Day.sule:Day.tu ≤ Day.mo⊢ Std.PRange.succMany? (Day.mo.toNat - Day.tu.toNat) Day.tu = some Day.mole:Day.tu ≤ Day.tu⊢ Std.PRange.succMany? (Day.tu.toNat - Day.tu.toNat) Day.tu = some Day.tule:Day.tu ≤ Day.we⊢ Std.PRange.succMany? (Day.we.toNat - Day.tu.toNat) Day.tu = some Day.wele:Day.tu ≤ Day.th⊢ Std.PRange.succMany? (Day.th.toNat - Day.tu.toNat) Day.tu = some Day.thle:Day.tu ≤ Day.fr⊢ Std.PRange.succMany? (Day.fr.toNat - Day.tu.toNat) Day.tu = some Day.frle:Day.tu ≤ Day.sa⊢ Std.PRange.succMany? (Day.sa.toNat - Day.tu.toNat) Day.tu = some Day.sale:Day.tu ≤ Day.su⊢ Std.PRange.succMany? (Day.su.toNat - Day.tu.toNat) Day.tu = some Day.sule:Day.we ≤ Day.mo⊢ Std.PRange.succMany? (Day.mo.toNat - Day.we.toNat) Day.we = some Day.mole:Day.we ≤ Day.tu⊢ Std.PRange.succMany? (Day.tu.toNat - Day.we.toNat) Day.we = some Day.tule:Day.we ≤ Day.we⊢ Std.PRange.succMany? (Day.we.toNat - Day.we.toNat) Day.we = some Day.wele:Day.we ≤ Day.th⊢ Std.PRange.succMany? (Day.th.toNat - Day.we.toNat) Day.we = some Day.thle:Day.we ≤ Day.fr⊢ Std.PRange.succMany? (Day.fr.toNat - Day.we.toNat) Day.we = some Day.frle:Day.we ≤ Day.sa⊢ Std.PRange.succMany? (Day.sa.toNat - Day.we.toNat) Day.we = some Day.sale:Day.we ≤ Day.su⊢ Std.PRange.succMany? (Day.su.toNat - Day.we.toNat) Day.we = some Day.sule:Day.th ≤ Day.mo⊢ Std.PRange.succMany? (Day.mo.toNat - Day.th.toNat) Day.th = some Day.mole:Day.th ≤ Day.tu⊢ Std.PRange.succMany? (Day.tu.toNat - Day.th.toNat) Day.th = some Day.tule:Day.th ≤ Day.we⊢ Std.PRange.succMany? (Day.we.toNat - Day.th.toNat) Day.th = some Day.wele:Day.th ≤ Day.th⊢ Std.PRange.succMany? (Day.th.toNat - Day.th.toNat) Day.th = some Day.thle:Day.th ≤ Day.fr⊢ Std.PRange.succMany? (Day.fr.toNat - Day.th.toNat) Day.th = some Day.frle:Day.th ≤ Day.sa⊢ Std.PRange.succMany? (Day.sa.toNat - Day.th.toNat) Day.th = some Day.sale:Day.th ≤ Day.su⊢ Std.PRange.succMany? (Day.su.toNat - Day.th.toNat) Day.th = some Day.sule:Day.fr ≤ Day.mo⊢ Std.PRange.succMany? (Day.mo.toNat - Day.fr.toNat) Day.fr = some Day.mole:Day.fr ≤ Day.tu⊢ Std.PRange.succMany? (Day.tu.toNat - Day.fr.toNat) Day.fr = some Day.tule:Day.fr ≤ Day.we⊢ Std.PRange.succMany? (Day.we.toNat - Day.fr.toNat) Day.fr = some Day.wele:Day.fr ≤ Day.th⊢ Std.PRange.succMany? (Day.th.toNat - Day.fr.toNat) Day.fr = some Day.thle:Day.fr ≤ Day.fr⊢ Std.PRange.succMany? (Day.fr.toNat - Day.fr.toNat) Day.fr = some Day.frle:Day.fr ≤ Day.sa⊢ Std.PRange.succMany? (Day.sa.toNat - Day.fr.toNat) Day.fr = some Day.sale:Day.fr ≤ Day.su⊢ Std.PRange.succMany? (Day.su.toNat - Day.fr.toNat) Day.fr = some Day.sule:Day.sa ≤ Day.mo⊢ Std.PRange.succMany? (Day.mo.toNat - Day.sa.toNat) Day.sa = some Day.mole:Day.sa ≤ Day.tu⊢ Std.PRange.succMany? (Day.tu.toNat - Day.sa.toNat) Day.sa = some Day.tule:Day.sa ≤ Day.we⊢ Std.PRange.succMany? (Day.we.toNat - Day.sa.toNat) Day.sa = some Day.wele:Day.sa ≤ Day.th⊢ Std.PRange.succMany? (Day.th.toNat - Day.sa.toNat) Day.sa = some Day.thle:Day.sa ≤ Day.fr⊢ Std.PRange.succMany? (Day.fr.toNat - Day.sa.toNat) Day.sa = some Day.frle:Day.sa ≤ Day.sa⊢ Std.PRange.succMany? (Day.sa.toNat - Day.sa.toNat) Day.sa = some Day.sale:Day.sa ≤ Day.su⊢ Std.PRange.succMany? (Day.su.toNat - Day.sa.toNat) Day.sa = some Day.sule:Day.su ≤ Day.mo⊢ Std.PRange.succMany? (Day.mo.toNat - Day.su.toNat) Day.su = some Day.mole:Day.su ≤ Day.tu⊢ Std.PRange.succMany? (Day.tu.toNat - Day.su.toNat) Day.su = some Day.tule:Day.su ≤ Day.we⊢ Std.PRange.succMany? (Day.we.toNat - Day.su.toNat) Day.su = some Day.wele:Day.su ≤ Day.th⊢ Std.PRange.succMany? (Day.th.toNat - Day.su.toNat) Day.su = some Day.thle:Day.su ≤ Day.fr⊢ Std.PRange.succMany? (Day.fr.toNat - Day.su.toNat) Day.su = some Day.frle:Day.su ≤ Day.sa⊢ Std.PRange.succMany? (Day.sa.toNat - Day.su.toNat) Day.su = some Day.sale:Day.su ≤ Day.su⊢ Std.PRange.succMany? (Day.su.toNat - Day.su.toNat) Day.su = some Day.su All goals completed! 🐙 le:Day.tu ≤ Day.mo⊢ Falsele:Day.we ≤ Day.mo⊢ Falsele:Day.we ≤ Day.tu⊢ Falsele:Day.th ≤ Day.mo⊢ Falsele:Day.th ≤ Day.tu⊢ Falsele:Day.th ≤ Day.we⊢ Falsele:Day.fr ≤ Day.mo⊢ Falsele:Day.fr ≤ Day.tu⊢ Falsele:Day.fr ≤ Day.we⊢ Falsele:Day.fr ≤ Day.th⊢ Falsele:Day.sa ≤ Day.mo⊢ Falsele:Day.sa ≤ Day.tu⊢ Falsele:Day.sa ≤ Day.we⊢ Falsele:Day.sa ≤ Day.th⊢ Falsele:Day.sa ≤ Day.fr⊢ Falsele:Day.su ≤ Day.mo⊢ Falsele:Day.su ≤ Day.tu⊢ Falsele:Day.su ≤ Day.we⊢ Falsele:Day.su ≤ Day.th⊢ Falsele:Day.su ≤ Day.fr⊢ Falsele:Day.su ≤ Day.sa⊢ False All goals completed! 🐙 d1:Dayd2:Day⊢ Std.PRange.UpwardEnumerable.LE d1 d2 → d1 ≤ d2 d1:Dayd2:Daysteps:Nateq:Std.PRange.succMany? steps d1 = some d2⊢ d1 ≤ d2 d1:Dayd2:Daysteps:Nateq:Std.PRange.succMany? steps d1 = some d2this:if d1 ≤ d2 then steps = d2.toNat - d1.toNat else False := Day.succMany?_steps eq⊢ d1 ≤ d2 d2: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 ≤ d2d2: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 ≤ d2d2: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 ≤ d2d2: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 ≤ d2d2: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 ≤ d2d2: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 ≤ d2d2: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 d2: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 ≤ d2d2: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 ≤ d2d2: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 ≤ d2d2: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 ≤ d2d2: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 ≤ d2d2: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 ≤ d2d2: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 steps: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.mosteps: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.tusteps: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.westeps: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.thsteps: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.frsteps: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.sasteps: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 steps: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.mosteps: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.tusteps: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.westeps: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.thsteps: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.frsteps: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.sasteps: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.susteps: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.mosteps: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.tusteps: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.westeps: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.thsteps: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.frsteps: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.sasteps: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.susteps: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.mosteps: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.tusteps: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.westeps: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.thsteps: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.frsteps: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.sasteps: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.susteps: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.mosteps: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.tusteps: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.westeps: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.thsteps: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.frsteps: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.sasteps: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.susteps: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.mosteps: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.tusteps: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.westeps: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.thsteps: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.frsteps: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.sasteps: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.susteps: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.mosteps: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.tusteps: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.westeps: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.thsteps: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.frsteps: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.sasteps: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.susteps: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.mosteps: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.tusteps: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.westeps: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.thsteps: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.frsteps: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.sasteps: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 steps: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 steps:Nateq:Std.PRange.succMany? steps Day.mo = some Day.mothis:Day.mo ≤ Day.mo ∧ steps = Day.mo.toNat - Day.mo.toNat⊢ Day.mo ≤ Day.mosteps:Nateq:Std.PRange.succMany? steps Day.mo = some Day.tuthis:Day.mo ≤ Day.tu ∧ steps = Day.tu.toNat - Day.mo.toNat⊢ Day.mo ≤ Day.tusteps:Nateq:Std.PRange.succMany? steps Day.mo = some Day.wethis:Day.mo ≤ Day.we ∧ steps = Day.we.toNat - Day.mo.toNat⊢ Day.mo ≤ Day.westeps:Nateq:Std.PRange.succMany? steps Day.mo = some Day.ththis:Day.mo ≤ Day.th ∧ steps = Day.th.toNat - Day.mo.toNat⊢ Day.mo ≤ Day.thsteps:Nateq:Std.PRange.succMany? steps Day.mo = some Day.frthis:Day.mo ≤ Day.fr ∧ steps = Day.fr.toNat - Day.mo.toNat⊢ Day.mo ≤ Day.frsteps:Nateq:Std.PRange.succMany? steps Day.mo = some Day.sathis:Day.mo ≤ Day.sa ∧ steps = Day.sa.toNat - Day.mo.toNat⊢ Day.mo ≤ Day.sasteps:Nateq:Std.PRange.succMany? steps Day.mo = some Day.suthis:Day.mo ≤ Day.su ∧ steps = Day.su.toNat - Day.mo.toNat⊢ Day.mo ≤ Day.susteps:Nateq:Std.PRange.succMany? steps Day.tu = some Day.mothis:Day.tu ≤ Day.mo ∧ steps = Day.mo.toNat - Day.tu.toNat⊢ Day.tu ≤ Day.mosteps:Nateq:Std.PRange.succMany? steps Day.tu = some Day.tuthis:Day.tu ≤ Day.tu ∧ steps = Day.tu.toNat - Day.tu.toNat⊢ Day.tu ≤ Day.tusteps:Nateq:Std.PRange.succMany? steps Day.tu = some Day.wethis:Day.tu ≤ Day.we ∧ steps = Day.we.toNat - Day.tu.toNat⊢ Day.tu ≤ Day.westeps:Nateq:Std.PRange.succMany? steps Day.tu = some Day.ththis:Day.tu ≤ Day.th ∧ steps = Day.th.toNat - Day.tu.toNat⊢ Day.tu ≤ Day.thsteps:Nateq:Std.PRange.succMany? steps Day.tu = some Day.frthis:Day.tu ≤ Day.fr ∧ steps = Day.fr.toNat - Day.tu.toNat⊢ Day.tu ≤ Day.frsteps:Nateq:Std.PRange.succMany? steps Day.tu = some Day.sathis:Day.tu ≤ Day.sa ∧ steps = Day.sa.toNat - Day.tu.toNat⊢ Day.tu ≤ Day.sasteps:Nateq:Std.PRange.succMany? steps Day.tu = some Day.suthis:Day.tu ≤ Day.su ∧ steps = Day.su.toNat - Day.tu.toNat⊢ Day.tu ≤ Day.susteps:Nateq:Std.PRange.succMany? steps Day.we = some Day.mothis:Day.we ≤ Day.mo ∧ steps = Day.mo.toNat - Day.we.toNat⊢ Day.we ≤ Day.mosteps:Nateq:Std.PRange.succMany? steps Day.we = some Day.tuthis:Day.we ≤ Day.tu ∧ steps = Day.tu.toNat - Day.we.toNat⊢ Day.we ≤ Day.tusteps:Nateq:Std.PRange.succMany? steps Day.we = some Day.wethis:Day.we ≤ Day.we ∧ steps = Day.we.toNat - Day.we.toNat⊢ Day.we ≤ Day.westeps:Nateq:Std.PRange.succMany? steps Day.we = some Day.ththis:Day.we ≤ Day.th ∧ steps = Day.th.toNat - Day.we.toNat⊢ Day.we ≤ Day.thsteps:Nateq:Std.PRange.succMany? steps Day.we = some Day.frthis:Day.we ≤ Day.fr ∧ steps = Day.fr.toNat - Day.we.toNat⊢ Day.we ≤ Day.frsteps:Nateq:Std.PRange.succMany? steps Day.we = some Day.sathis:Day.we ≤ Day.sa ∧ steps = Day.sa.toNat - Day.we.toNat⊢ Day.we ≤ Day.sasteps:Nateq:Std.PRange.succMany? steps Day.we = some Day.suthis:Day.we ≤ Day.su ∧ steps = Day.su.toNat - Day.we.toNat⊢ Day.we ≤ Day.susteps:Nateq:Std.PRange.succMany? steps Day.th = some Day.mothis:Day.th ≤ Day.mo ∧ steps = Day.mo.toNat - Day.th.toNat⊢ Day.th ≤ Day.mosteps:Nateq:Std.PRange.succMany? steps Day.th = some Day.tuthis:Day.th ≤ Day.tu ∧ steps = Day.tu.toNat - Day.th.toNat⊢ Day.th ≤ Day.tusteps:Nateq:Std.PRange.succMany? steps Day.th = some Day.wethis:Day.th ≤ Day.we ∧ steps = Day.we.toNat - Day.th.toNat⊢ Day.th ≤ Day.westeps:Nateq:Std.PRange.succMany? steps Day.th = some Day.ththis:Day.th ≤ Day.th ∧ steps = Day.th.toNat - Day.th.toNat⊢ Day.th ≤ Day.thsteps:Nateq:Std.PRange.succMany? steps Day.th = some Day.frthis:Day.th ≤ Day.fr ∧ steps = Day.fr.toNat - Day.th.toNat⊢ Day.th ≤ Day.frsteps:Nateq:Std.PRange.succMany? steps Day.th = some Day.sathis:Day.th ≤ Day.sa ∧ steps = Day.sa.toNat - Day.th.toNat⊢ Day.th ≤ Day.sasteps:Nateq:Std.PRange.succMany? steps Day.th = some Day.suthis:Day.th ≤ Day.su ∧ steps = Day.su.toNat - Day.th.toNat⊢ Day.th ≤ Day.susteps:Nateq:Std.PRange.succMany? steps Day.fr = some Day.mothis:Day.fr ≤ Day.mo ∧ steps = Day.mo.toNat - Day.fr.toNat⊢ Day.fr ≤ Day.mosteps:Nateq:Std.PRange.succMany? steps Day.fr = some Day.tuthis:Day.fr ≤ Day.tu ∧ steps = Day.tu.toNat - Day.fr.toNat⊢ Day.fr ≤ Day.tusteps:Nateq:Std.PRange.succMany? steps Day.fr = some Day.wethis:Day.fr ≤ Day.we ∧ steps = Day.we.toNat - Day.fr.toNat⊢ Day.fr ≤ Day.westeps:Nateq:Std.PRange.succMany? steps Day.fr = some Day.ththis:Day.fr ≤ Day.th ∧ steps = Day.th.toNat - Day.fr.toNat⊢ Day.fr ≤ Day.thsteps:Nateq:Std.PRange.succMany? steps Day.fr = some Day.frthis:Day.fr ≤ Day.fr ∧ steps = Day.fr.toNat - Day.fr.toNat⊢ Day.fr ≤ Day.frsteps:Nateq:Std.PRange.succMany? steps Day.fr = some Day.sathis:Day.fr ≤ Day.sa ∧ steps = Day.sa.toNat - Day.fr.toNat⊢ Day.fr ≤ Day.sasteps:Nateq:Std.PRange.succMany? steps Day.fr = some Day.suthis:Day.fr ≤ Day.su ∧ steps = Day.su.toNat - Day.fr.toNat⊢ Day.fr ≤ Day.susteps:Nateq:Std.PRange.succMany? steps Day.sa = some Day.mothis:Day.sa ≤ Day.mo ∧ steps = Day.mo.toNat - Day.sa.toNat⊢ Day.sa ≤ Day.mosteps:Nateq:Std.PRange.succMany? steps Day.sa = some Day.tuthis:Day.sa ≤ Day.tu ∧ steps = Day.tu.toNat - Day.sa.toNat⊢ Day.sa ≤ Day.tusteps:Nateq:Std.PRange.succMany? steps Day.sa = some Day.wethis:Day.sa ≤ Day.we ∧ steps = Day.we.toNat - Day.sa.toNat⊢ Day.sa ≤ Day.westeps:Nateq:Std.PRange.succMany? steps Day.sa = some Day.ththis:Day.sa ≤ Day.th ∧ steps = Day.th.toNat - Day.sa.toNat⊢ Day.sa ≤ Day.thsteps:Nateq:Std.PRange.succMany? steps Day.sa = some Day.frthis:Day.sa ≤ Day.fr ∧ steps = Day.fr.toNat - Day.sa.toNat⊢ Day.sa ≤ Day.frsteps:Nateq:Std.PRange.succMany? steps Day.sa = some Day.sathis:Day.sa ≤ Day.sa ∧ steps = Day.sa.toNat - Day.sa.toNat⊢ Day.sa ≤ Day.sasteps:Nateq:Std.PRange.succMany? steps Day.sa = some Day.suthis:Day.sa ≤ Day.su ∧ steps = Day.su.toNat - Day.sa.toNat⊢ Day.sa ≤ Day.susteps:Nateq:Std.PRange.succMany? steps Day.su = some Day.mothis:Day.su ≤ Day.mo ∧ steps = Day.mo.toNat - Day.su.toNat⊢ Day.su ≤ Day.mosteps:Nateq:Std.PRange.succMany? steps Day.su = some Day.tuthis:Day.su ≤ Day.tu ∧ steps = Day.tu.toNat - Day.su.toNat⊢ Day.su ≤ Day.tusteps:Nateq:Std.PRange.succMany? steps Day.su = some Day.wethis:Day.su ≤ Day.we ∧ steps = Day.we.toNat - Day.su.toNat⊢ Day.su ≤ Day.westeps:Nateq:Std.PRange.succMany? steps Day.su = some Day.ththis:Day.su ≤ Day.th ∧ steps = Day.th.toNat - Day.su.toNat⊢ Day.su ≤ Day.thsteps:Nateq:Std.PRange.succMany? steps Day.su = some Day.frthis:Day.su ≤ Day.fr ∧ steps = Day.fr.toNat - Day.su.toNat⊢ Day.su ≤ Day.frsteps:Nateq:Std.PRange.succMany? steps Day.su = some Day.sathis:Day.su ≤ Day.sa ∧ steps = Day.sa.toNat - Day.su.toNat⊢ Day.su ≤ Day.sasteps: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 steps: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 steps:Nateq:Std.PRange.succMany? steps Day.mo = some Day.moleft✝:Day.mo ≤ Day.moright✝:steps = Day.mo.toNat - Day.mo.toNat⊢ Day.mo ≤ Day.mosteps:Nateq:Std.PRange.succMany? steps Day.mo = some Day.tuleft✝:Day.mo ≤ Day.turight✝:steps = Day.tu.toNat - Day.mo.toNat⊢ Day.mo ≤ Day.tusteps:Nateq:Std.PRange.succMany? steps Day.mo = some Day.weleft✝:Day.mo ≤ Day.weright✝:steps = Day.we.toNat - Day.mo.toNat⊢ Day.mo ≤ Day.westeps:Nateq:Std.PRange.succMany? steps Day.mo = some Day.thleft✝:Day.mo ≤ Day.thright✝:steps = Day.th.toNat - Day.mo.toNat⊢ Day.mo ≤ Day.thsteps:Nateq:Std.PRange.succMany? steps Day.mo = some Day.frleft✝:Day.mo ≤ Day.frright✝:steps = Day.fr.toNat - Day.mo.toNat⊢ Day.mo ≤ Day.frsteps:Nateq:Std.PRange.succMany? steps Day.mo = some Day.saleft✝:Day.mo ≤ Day.saright✝:steps = Day.sa.toNat - Day.mo.toNat⊢ Day.mo ≤ Day.sasteps:Nateq:Std.PRange.succMany? steps Day.mo = some Day.suleft✝:Day.mo ≤ Day.suright✝:steps = Day.su.toNat - Day.mo.toNat⊢ Day.mo ≤ Day.susteps:Nateq:Std.PRange.succMany? steps Day.tu = some Day.moleft✝:Day.tu ≤ Day.moright✝:steps = Day.mo.toNat - Day.tu.toNat⊢ Day.tu ≤ Day.mosteps:Nateq:Std.PRange.succMany? steps Day.tu = some Day.tuleft✝:Day.tu ≤ Day.turight✝:steps = Day.tu.toNat - Day.tu.toNat⊢ Day.tu ≤ Day.tusteps:Nateq:Std.PRange.succMany? steps Day.tu = some Day.weleft✝:Day.tu ≤ Day.weright✝:steps = Day.we.toNat - Day.tu.toNat⊢ Day.tu ≤ Day.westeps:Nateq:Std.PRange.succMany? steps Day.tu = some Day.thleft✝:Day.tu ≤ Day.thright✝:steps = Day.th.toNat - Day.tu.toNat⊢ Day.tu ≤ Day.thsteps:Nateq:Std.PRange.succMany? steps Day.tu = some Day.frleft✝:Day.tu ≤ Day.frright✝:steps = Day.fr.toNat - Day.tu.toNat⊢ Day.tu ≤ Day.frsteps:Nateq:Std.PRange.succMany? steps Day.tu = some Day.saleft✝:Day.tu ≤ Day.saright✝:steps = Day.sa.toNat - Day.tu.toNat⊢ Day.tu ≤ Day.sasteps:Nateq:Std.PRange.succMany? steps Day.tu = some Day.suleft✝:Day.tu ≤ Day.suright✝:steps = Day.su.toNat - Day.tu.toNat⊢ Day.tu ≤ Day.susteps:Nateq:Std.PRange.succMany? steps Day.we = some Day.moleft✝:Day.we ≤ Day.moright✝:steps = Day.mo.toNat - Day.we.toNat⊢ Day.we ≤ Day.mosteps:Nateq:Std.PRange.succMany? steps Day.we = some Day.tuleft✝:Day.we ≤ Day.turight✝:steps = Day.tu.toNat - Day.we.toNat⊢ Day.we ≤ Day.tusteps:Nateq:Std.PRange.succMany? steps Day.we = some Day.weleft✝:Day.we ≤ Day.weright✝:steps = Day.we.toNat - Day.we.toNat⊢ Day.we ≤ Day.westeps:Nateq:Std.PRange.succMany? steps Day.we = some Day.thleft✝:Day.we ≤ Day.thright✝:steps = Day.th.toNat - Day.we.toNat⊢ Day.we ≤ Day.thsteps:Nateq:Std.PRange.succMany? steps Day.we = some Day.frleft✝:Day.we ≤ Day.frright✝:steps = Day.fr.toNat - Day.we.toNat⊢ Day.we ≤ Day.frsteps:Nateq:Std.PRange.succMany? steps Day.we = some Day.saleft✝:Day.we ≤ Day.saright✝:steps = Day.sa.toNat - Day.we.toNat⊢ Day.we ≤ Day.sasteps:Nateq:Std.PRange.succMany? steps Day.we = some Day.suleft✝:Day.we ≤ Day.suright✝:steps = Day.su.toNat - Day.we.toNat⊢ Day.we ≤ Day.susteps:Nateq:Std.PRange.succMany? steps Day.th = some Day.moleft✝:Day.th ≤ Day.moright✝:steps = Day.mo.toNat - Day.th.toNat⊢ Day.th ≤ Day.mosteps:Nateq:Std.PRange.succMany? steps Day.th = some Day.tuleft✝:Day.th ≤ Day.turight✝:steps = Day.tu.toNat - Day.th.toNat⊢ Day.th ≤ Day.tusteps:Nateq:Std.PRange.succMany? steps Day.th = some Day.weleft✝:Day.th ≤ Day.weright✝:steps = Day.we.toNat - Day.th.toNat⊢ Day.th ≤ Day.westeps:Nateq:Std.PRange.succMany? steps Day.th = some Day.thleft✝:Day.th ≤ Day.thright✝:steps = Day.th.toNat - Day.th.toNat⊢ Day.th ≤ Day.thsteps:Nateq:Std.PRange.succMany? steps Day.th = some Day.frleft✝:Day.th ≤ Day.frright✝:steps = Day.fr.toNat - Day.th.toNat⊢ Day.th ≤ Day.frsteps:Nateq:Std.PRange.succMany? steps Day.th = some Day.saleft✝:Day.th ≤ Day.saright✝:steps = Day.sa.toNat - Day.th.toNat⊢ Day.th ≤ Day.sasteps:Nateq:Std.PRange.succMany? steps Day.th = some Day.suleft✝:Day.th ≤ Day.suright✝:steps = Day.su.toNat - Day.th.toNat⊢ Day.th ≤ Day.susteps:Nateq:Std.PRange.succMany? steps Day.fr = some Day.moleft✝:Day.fr ≤ Day.moright✝:steps = Day.mo.toNat - Day.fr.toNat⊢ Day.fr ≤ Day.mosteps:Nateq:Std.PRange.succMany? steps Day.fr = some Day.tuleft✝:Day.fr ≤ Day.turight✝:steps = Day.tu.toNat - Day.fr.toNat⊢ Day.fr ≤ Day.tusteps:Nateq:Std.PRange.succMany? steps Day.fr = some Day.weleft✝:Day.fr ≤ Day.weright✝:steps = Day.we.toNat - Day.fr.toNat⊢ Day.fr ≤ Day.westeps:Nateq:Std.PRange.succMany? steps Day.fr = some Day.thleft✝:Day.fr ≤ Day.thright✝:steps = Day.th.toNat - Day.fr.toNat⊢ Day.fr ≤ Day.thsteps:Nateq:Std.PRange.succMany? steps Day.fr = some Day.frleft✝:Day.fr ≤ Day.frright✝:steps = Day.fr.toNat - Day.fr.toNat⊢ Day.fr ≤ Day.frsteps:Nateq:Std.PRange.succMany? steps Day.fr = some Day.saleft✝:Day.fr ≤ Day.saright✝:steps = Day.sa.toNat - Day.fr.toNat⊢ Day.fr ≤ Day.sasteps:Nateq:Std.PRange.succMany? steps Day.fr = some Day.suleft✝:Day.fr ≤ Day.suright✝:steps = Day.su.toNat - Day.fr.toNat⊢ Day.fr ≤ Day.susteps:Nateq:Std.PRange.succMany? steps Day.sa = some Day.moleft✝:Day.sa ≤ Day.moright✝:steps = Day.mo.toNat - Day.sa.toNat⊢ Day.sa ≤ Day.mosteps:Nateq:Std.PRange.succMany? steps Day.sa = some Day.tuleft✝:Day.sa ≤ Day.turight✝:steps = Day.tu.toNat - Day.sa.toNat⊢ Day.sa ≤ Day.tusteps:Nateq:Std.PRange.succMany? steps Day.sa = some Day.weleft✝:Day.sa ≤ Day.weright✝:steps = Day.we.toNat - Day.sa.toNat⊢ Day.sa ≤ Day.westeps:Nateq:Std.PRange.succMany? steps Day.sa = some Day.thleft✝:Day.sa ≤ Day.thright✝:steps = Day.th.toNat - Day.sa.toNat⊢ Day.sa ≤ Day.thsteps:Nateq:Std.PRange.succMany? steps Day.sa = some Day.frleft✝:Day.sa ≤ Day.frright✝:steps = Day.fr.toNat - Day.sa.toNat⊢ Day.sa ≤ Day.frsteps:Nateq:Std.PRange.succMany? steps Day.sa = some Day.saleft✝:Day.sa ≤ Day.saright✝:steps = Day.sa.toNat - Day.sa.toNat⊢ Day.sa ≤ Day.sasteps:Nateq:Std.PRange.succMany? steps Day.sa = some Day.suleft✝:Day.sa ≤ Day.suright✝:steps = Day.su.toNat - Day.sa.toNat⊢ Day.sa ≤ Day.susteps:Nateq:Std.PRange.succMany? steps Day.su = some Day.moleft✝:Day.su ≤ Day.moright✝:steps = Day.mo.toNat - Day.su.toNat⊢ Day.su ≤ Day.mosteps:Nateq:Std.PRange.succMany? steps Day.su = some Day.tuleft✝:Day.su ≤ Day.turight✝:steps = Day.tu.toNat - Day.su.toNat⊢ Day.su ≤ Day.tusteps:Nateq:Std.PRange.succMany? steps Day.su = some Day.weleft✝:Day.su ≤ Day.weright✝:steps = Day.we.toNat - Day.su.toNat⊢ Day.su ≤ Day.westeps:Nateq:Std.PRange.succMany? steps Day.su = some Day.thleft✝:Day.su ≤ Day.thright✝:steps = Day.th.toNat - Day.su.toNat⊢ Day.su ≤ Day.thsteps:Nateq:Std.PRange.succMany? steps Day.su = some Day.frleft✝:Day.su ≤ Day.frright✝:steps = Day.fr.toNat - Day.su.toNat⊢ Day.su ≤ Day.frsteps:Nateq:Std.PRange.succMany? steps Day.su = some Day.saleft✝:Day.su ≤ Day.saright✝:steps = Day.sa.toNat - Day.su.toNat⊢ Day.su ≤ Day.sasteps: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 All goals completed! 🐙

It is now possible to iterate over ranges of days:

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
Live ↪

20.18.4. Ranges and Slices

Range syntax can be used with data structures that support slicing to select a slice of the structure.

Slicing Lists

Lists may be sliced with any of the interval types:

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"]
Live ↪
Custom Slices

A Triple contains three values of the same type:

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

Positions in a triple may be any of the fields, or just after thd:

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

A slice of a triple consists of a triple, a starting position, and a stopping position. The starting position is inclusive, and the stopping position exclusive:

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

Ranges of TriplePos can be used to select a slice from a triple by implementing instances of each supported range type's Sliceable class. For example, Std.Rco.Sliceable allows left-closed, right-open ranges to be used to slice Triples:

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 }

Infinite ranges have only a lower bound:

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 }
Live ↪
🔗type class
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)

This typeclass indicates how to obtain slices of elements of α over ranges in the index type β, the ranges being left-closed right-open.

The type of resulting the slices is γ.

Instance Constructor

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

Methods

mkSlice : α → Std.Rco β → γ

Slices carrier from range.lower (inclusive) to range.upper (exclusive).

🔗type class
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)

This typeclass indicates how to obtain slices of elements of α over ranges in the index type β, the ranges being closed.

The type of the resulting slices is γ.

Instance Constructor

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

Methods

mkSlice : α → Std.Rcc β → γ

Slices carrier from range.lower to range.upper, both inclusive.

🔗type class
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)

This typeclass indicates how to obtain slices of elements of α over ranges in the index type β, the ranges being left-closed right-unbounded.

The type of the resulting slices is γ.

Instance Constructor

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

Methods

mkSlice : α → Std.Rci β → γ

Slices carrier from range.lower (inclusive).

🔗type class
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)

This typeclass indicates how to obtain slices of elements of α over ranges in the index type β, the ranges being open.

The type of the resulting slices is γ.

Instance Constructor

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

Methods

mkSlice : α → Std.Roo β → γ

Slices carrier from range.lower to range.upper, both exclusive.

🔗type class
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)

This typeclass indicates how to obtain slices of elements of α over ranges in the index type β, the ranges being left-open right-closed.

The type of the resulting slices is γ.

Instance Constructor

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

Methods

mkSlice : α → Std.Roc β → γ

Slices carrier from range.lower (exclusive) to range.upper (inclusive).

🔗type class
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)

This typeclass indicates how to obtain slices of elements of α over ranges in the index type β, the ranges being left-open right-unbounded.

The type of the resulting slices is γ.

Instance Constructor

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

Methods

mkSlice : α → Std.Roi β → γ

Slices carrier from range.lower (exclusive).

🔗type class
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)

This typeclass indicates how to obtain slices of elements of α over ranges in the index type β, the ranges being left-unbounded right-open.

The type of the resulting slices is γ.

Instance Constructor

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

Methods

mkSlice : α → Std.Rio β → γ

Slices carrier up to range.upper (exclusive).

🔗type class
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)

This typeclass indicates how to obtain slices of elements of α over ranges in the index type β, the ranges being left-unbounded right-closed.

The type of the resulting slices is γ.

Instance Constructor

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

Methods

mkSlice : α → Std.Ric β → γ

Slices carrier up to range.upper (inclusive).

🔗type class
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)

This typeclass indicates how to obtain slices of elements of α over the full range in the index type β.

The type of the resulting slices is γ.

Instance Constructor

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

Methods

mkSlice : α → Std.Rii β → γ

Slices carrier with no bounds.