test: use <|> at binop_lazy test

This commit is contained in:
Leonardo de Moura 2021-09-07 17:10:36 -07:00
parent 2f0a936f88
commit c5f9113dcf

View file

@ -1,20 +1,10 @@
class HOrElse' (α : Type u) (β : Type v) (γ : outParam (Type w)) where
hOrElse' : α → (Unit → β) → γ
infixr:20 " <%> " => HOrElse.hOrElse'
macro_rules | `($x <%> $y) => `(binop_lazy% HOrElse'.hOrElse' $x $y)
instance : HOrElse' (IO α) (IO α) (IO α) where
hOrElse' a b := try a catch _ => b ()
def f : IO Unit :=
(do IO.println "case 1"; throw (IO.userError "failed"))
<%>
<|>
(do IO.println "case 2"; throw (IO.userError "failed"))
<%>
<|>
(do IO.println "case 3")
<%>
<|>
(let x := dbg_trace "hello"; 1
IO.println x)