summaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2019-08-10 13:02:21 -0400
committerGravatar Adam Chlipala <adam@chlipala.net>2019-08-10 13:02:21 -0400
commit52eb84c63a458e2a042c8fe451e96a11fdaeb4ed (patch)
tree4016c5954628f8d1ed11249c09f0fdbc7419d33f /lib
parent6273c4602a8103f23856616966c34721ad726d3e (diff)
Datetime.ord_month
Diffstat (limited to 'lib')
-rw-r--r--lib/ur/datetime.ur3
-rw-r--r--lib/ur/datetime.urs1
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