blob: 6b04d291f71aff972e082b3350801731d96fd132 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
|
(*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.maybe 'a -> 'a*)
(*let fromJust op= match op with | Just v -> v | Nothing -> failwith "fromJust of Nothing" end*)
val _ = export_theory()
|
