Datetime.ord_month

2 files changed, 3 insertions, 1 deletions

diff --git a/lib/ur/datetime.ur b/lib/ur/datetime.ur
index 9aeab291..99fd5a7d 100644
--- a/lib/ur/datetime.ur
+++ b/lib/ur/datetime.ur
@@ -88,7 +88,8 @@ fun intToMonth i = case i of
                      | n => error <xml>Invalid month number {[n]}</xml>
 
 val eq_month = mkEq (fn a b => monthToInt a = monthToInt b)
-
+val ord_month = mkOrd {Lt = fn a b => monthToInt a < monthToInt b,
+                       Le = fn a b => monthToInt a <= monthToInt b}
 
 fun toTime dt : time = fromDatetime dt.Year (monthToInt dt.Month) dt.Day
                                     dt.Hour dt.Minute dt.Second
diff --git a/lib/ur/datetime.urs b/lib/ur/datetime.urs
index 972f86bf..f8460443 100644
--- a/lib/ur/datetime.urs
+++ b/lib/ur/datetime.urs
@@ -20,6 +20,7 @@ val show_day_of_week : show day_of_week
 val show_month : show month
 val eq_day_of_week : eq day_of_week
 val eq_month : eq month
+val ord_month : ord month
 val dayOfWeekToInt : day_of_week -> int
 val intToDayOfWeek : int -> day_of_week
 val monthToInt : month -> int