blob: 22d7e061261627cc30a7ea360629bac2d50a9baf (
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 'a -> 'a*)
(*let fromJust op= match op with | Just v -> v | Nothing -> failwith "fromJust of Nothing" end*)
val _ = export_theory()
|
