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