summaryrefslogtreecommitdiff
path: root/lib/ur/datetime.urs
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/ur/datetime.urs
parent6273c4602a8103f23856616966c34721ad726d3e (diff)
Datetime.ord_month
Diffstat (limited to 'lib/ur/datetime.urs')
-rw-r--r--lib/ur/datetime.urs1
1 files changed, 1 insertions, 0 deletions
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