Theory Lem_maybe_extra

chapter ‹Generated by Lem from maybe_extra.lem›.›

theory "Lem_maybe_extra" 

imports
  Main
  "Lem_basic_classes"
  "Lem_maybe"
  "Lem_assert_extra"

begin 

 

― ‹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›

end