Equations
- ⋯ = ⋯
Equations
- Time.instCoeOutIccNatInt a b = { coe := fun (n : Time.Icc a b) => ↑n.val }
Equations
- Time.instCoeOutIco a b = { coe := fun (n : Time.Ico a b) => n.val }
instance
Time.instLeReflIco
{α : Type}
[LE α]
[LT α]
[Time.LeRefl α]
{a b : α}
:
Time.LeRefl (Time.Ico a b)
Equations
- ⋯ = ⋯
Equations
- Time.instCoeOutIcoNat a b = { coe := fun (n : Time.Ico a b) => n.val }
Equations
- Time.instCoeOutIcoNatInt a b = { coe := fun (n : Time.Ico a b) => ↑n.val }
- icc : Time.Icc a b
Instances For
instance
Time.instCoeNonemptyIccIcc
{α : Type}
[LE α]
[Time.LeRefl α]
(a b : α)
:
Coe (Time.NonemptyIcc a b) (Time.Icc a b)
Equations
- Time.instCoeNonemptyIccIcc a b = { coe := fun (n : Time.NonemptyIcc a b) => n.icc }
- ico : Time.Ico a b
Instances For
instance
Time.instCoeNonemptyIcoIco
{α : Type}
[LE α]
[LT α]
[Time.LeRefl α]
(a b : α)
:
Coe (Time.NonemptyIco a b) (Time.Ico a b)
Equations
- Time.instCoeNonemptyIcoIco a b = { coe := fun (n : Time.NonemptyIco a b) => n.ico }
def
Time.toNonemptyIcc
{α : Type}
[LE α]
[Time.LeRefl α]
{a b : α}
(v : Time.Icc a b)
(h : a ≤ b)
:
Time.NonemptyIcc a b
Equations
- Time.toNonemptyIcc v h = { icc := v, isNonempty := ⋯ }
Instances For
def
Time.toNonemptyIco
{α : Type}
[LE α]
[LT α]
[Time.LeRefl α]
{a b : α}
(v : Time.Ico a b)
(h : a < b)
:
Time.NonemptyIco a b
Equations
- Time.toNonemptyIco v h = { ico := v, isNonempty := ⋯ }
Instances For
Instances For
instance
Time.NonemptyIcc.instCoeNatFinHSubHAddOfNat
{n m : Nat}
:
Coe (Time.NonemptyIcc n m) (Fin (m + 1 - n))
Equations
- Time.NonemptyIcc.instCoeNatFinHSubHAddOfNat = { coe := fun (x : Time.NonemptyIcc n m) => x.toFin }
Equations
- Time.NonemptyIcc.instCoeNatOfNatFin = { coe := fun (x : Time.NonemptyIcc 1 m) => Fin.cast ⋯ x.toFin }