blob: 0a57814c310448a51afc10f5da9ff3719f9ebd94 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
|
chapter \<open>Generated by Lem from maybe_extra.lem.\<close>
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
|
