diff options
Diffstat (limited to 'snapshots/hol4/lem/hol-lib/lem_maybe_extraScript.sml')
| -rw-r--r-- | snapshots/hol4/lem/hol-lib/lem_maybe_extraScript.sml | 23 |
1 files changed, 23 insertions, 0 deletions
diff --git a/snapshots/hol4/lem/hol-lib/lem_maybe_extraScript.sml b/snapshots/hol4/lem/hol-lib/lem_maybe_extraScript.sml new file mode 100644 index 00000000..6b04d291 --- /dev/null +++ b/snapshots/hol4/lem/hol-lib/lem_maybe_extraScript.sml @@ -0,0 +1,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() + |