-----------------------------------------------------------------------

--------------------Start Vector3 Utilities----------------------------

-----------------------------------------------------------------------

@[implicit_reducible]

instance Lean4Itree.instOfNatULiftFin2Zero {n : ℕ} [Fin2.IsLT 0 n] : OfNat (ULift.{u_1, 0} (Fin2 n)) 0

Equations

• Lean4Itree.instOfNatULiftFin2Zero = { ofNat := { down := Fin2.ofNat' 0 } }

@[implicit_reducible]

instance Lean4Itree.instOfNatULiftFin2One {n : ℕ} [Fin2.IsLT 1 n] : OfNat (ULift.{u_1, 0} (Fin2 n)) 1

Equations

• Lean4Itree.instOfNatULiftFin2One = { ofNat := { down := Fin2.ofNat' 1 } }

def Lean4Itree.elim0 {α : Sort u} (i : ULift.{u_1, 0} (Fin2 0)) : α

The empty eliminator out of ULift (Fin2 0): a lifted Fin2 0 has no inhabitant.

Equations

• Lean4Itree.elim0 i = i.down.elim0

def Lean4Itree.fin1Const {α : Sort u_1} (v : α) (i : ULift.{u_2, 0} (Fin2 1)) : α

The constant function ULift (Fin2 1) → α returning v at the unique index.

Equations

• Lean4Itree.fin1Const v i = match i.down with | Fin2.fz => v

def Lean4Itree.fin2Const {α : Type u_1} (x y : α) (i : ULift.{u_2, 0} (Fin2 2)) : α

The function ULift (Fin2 2) → α returning x at index 0 and y at index 1.

Equations

• Lean4Itree.fin2Const x y i = [x, y] i.down

theorem Lean4Itree.elim0_eq_all {α : Sort u_1} (x : ULift.{u_2, 0} (Fin2 0) → α) : x = elim0

theorem Lean4Itree.fin1Const_inj {α : Sort u_1} {x y : α} (h : fin1Const x = fin1Const y) : x = y

theorem Lean4Itree.fin1Const_fin0 {α✝ : Sort u_1} {c : ULift.{u_2, 0} (Fin2 1) → α✝} : fin1Const (c 0) = c

-----------------------------------------------------------------------

--------------------End Vector3 Utilities------------------------------

-----------------------------------------------------------------------

-----------------------------------------------------------------------

--------------------Start PFunctor Utilities---------------------------

-----------------------------------------------------------------------

theorem Lean4Itree.PFunctor.M.unfold_corec'_left {P : PFunctor.{uA, uB}} {α : Type u} (F : P.M ⊕ α → ↑P (P.M ⊕ α)) (h_eq : ∀ (l : P.M), F (Sum.inl l) = ⟨l.dest.fst, Sum.inl ∘ l.dest.snd⟩) (l : P.M) : PFunctor.M.corec F (Sum.inl l) = l

theorem Lean4Itree.PFunctor.M.unfold_corec' {P : PFunctor.{uA, uB}} {α : Type u} (F : {X : Type (max u uA uB)} → (α → X) → α → P.M ⊕ ↑P X) (x : α) : PFunctor.M.corec' (fun {X : Type (max u uA uB)} => F) x = match F Sum.inr x with | Sum.inl l => l | Sum.inr ⟨a, g⟩ => PFunctor.M.mk ⟨a, fun (i : P.B a) => match g i with | Sum.inl l => l | Sum.inr r => PFunctor.M.corec' (fun {X : Type (max u uA uB)} => F) r⟩

-----------------------------------------------------------------------

--------------------End PFunctor Utilities---------------------------

-----------------------------------------------------------------------