decidable lt comparison function

a44a5155 · Sven Wille · 62014655 · a44a5155 · a44a5155
Commit a44a5155 authored 5 years ago by Sven Wille
--- a/errors/mmt-omdoc/math.mmt.err
+++ b/errors/mmt-omdoc/math.mmt.err
-<errors>
-</errors>
--- a/source/math.mmt
+++ b/source/math.mmt
@@ -272,6 +272,8 @@ theory OptionType : ur:?PLF =
 	None : {A : 𝒰 100} Option A ❘ # None ❙
 	None_is_not_Defined : {A : 𝒰 100} ⊦ isDefined (None A) ≐ false ❙
 	Not_None_is_Defined : {A, a : Option A} ⊦ (a ≠ None A) ⟶ ⊦ isDefined a ❙
+
+	Some : {A : 𝒰 100} A ⟶  Option A ❙
 ❚

 theory DescriptionOperator : ur:?PLF =