α : Type u
β : Type v
γ : Type w
c₁ : Computation α
a : α
⊢ destruct ({ hOrElse := fun a b => OrElse.orElse a b }.1 (think c₁) fun x => pure a) = Sum.inl a
α : Type u
β : Type v
γ : Type w
c₁ : Computation α
a : α
⊢ destruct (HOrElse.hOrElse (think c₁) fun x => pure a) = Sum.inl a
unfold HOrElse.hOrElse instHOrElse
α : Type u
β : Type v
γ : Type w
c₁ : Computation α
a : α
⊢ destruct
      ({
            hOrElse := fun a b =>
              {
                    orElse :=
                      (let src := monad;
                        Alternative.mk empty @orElse).3 }.1
                a b }.1
        (think c₁) fun x => pure a) =
    Sum.inl a
α : Type u
β : Type v
γ : Type w
c₁ : Computation α
a : α
⊢ destruct ({ hOrElse := fun a b => OrElse.orElse a b }.1 (think c₁) fun x => pure a) = Sum.inl a
unfold OrElse.orElse instOrElse Alternative.orElse instAlternativeComputation
no goals
α : Type u
β : Type v
γ : Type w
c₁ : Computation α
a : α
⊢ destruct
      ({
            hOrElse := fun a b =>
              {
                    orElse :=
                      (let src := monad;
                        Alternative.mk empty @orElse).3 }.1
                a b }.1
        (think c₁) fun x => pure a) =
    Sum.inl a
simp [orElse]