(*Generated by Lem from maybe_extra.lem.*)
open HolKernel Parse boolLib bossLib;
open lem_basic_classesTheory lem_maybeTheory lem_assert_extraTheory;

val _ = numLib.prefer_num();



val _ = new_theory "lem_maybe_extra"

 

(*open import Basic_classes Maybe Assert_extra*)

(* ----------------------- *)
(* fromJust                *)
(* ----------------------- *)

(*val fromJust : forall 'a. maybe 'a -> 'a*)
(*let fromJust op=  match op with | Just v -> v | Nothing -> failwith "fromJust of Nothing" end*)

val _ = export_theory()