maybe.egi

--
--
-- Maybe (Option)
--
--

inductive pattern Maybe a :=
  | nothing
  | just a

inductive Maybe a :=
  | Nothing
  | Just a

def maybe {a} (m: Matcher a) : Matcher (Maybe a) :=
  matcher
    | nothing as () with
      | Nothing -> [()]
      | _ -> []
    | just $ as (m) with
      | Just $x -> [x]
      | _ -> []
    | $ as (something) with
      | $tgt -> [tgt]