module Meta.Alt where
record Alt (M : Effect) : Typeω where
  private module M = Effect M
  field
    fail  :  {} {A : Type }  M.₀ A
    _<|>_ :  {} {A : Type }  M.₀ A  M.₀ A  M.₀ A

  infixl 3 _<|>_

open Alt  ...  public

guard
  :  {M : Effect} (let module M = Effect M)  appl : Idiom M   alt : Alt M 
   Bool  M.₀ 
guard true = pure tt
guard false = fail

guardM
  :  {M : Effect} (let module M = Effect M)  mon : Bind M   alt : Alt M 
   M.₀ Bool  M.₀ 
guardM M = M >>= guard