summaryrefslogtreecommitdiff
path: root/lib/ur/top.urs
diff options
context:
space:
mode:
authorGravatar Ziv Scully <ziv@mit.edu>2015-07-19 19:05:16 -0700
committerGravatar Ziv Scully <ziv@mit.edu>2015-07-19 19:05:16 -0700
commita197d648e075a696f5ca86b23913b668f2baf940 (patch)
tree4c044e00c2df8ca6fd76d072f05bf1e3ff202140 /lib/ur/top.urs
parentbc38beafd07b7ae6106a2fffda82084a08af7f06 (diff)
parentc6e4d352f01eff2ddcdcc53c0f2a14666c2af8b2 (diff)
Merge.
Diffstat (limited to 'lib/ur/top.urs')
-rw-r--r--lib/ur/top.urs7
1 files changed, 7 insertions, 0 deletions
diff --git a/lib/ur/top.urs b/lib/ur/top.urs
index 15bc6a22..8273db0c 100644
--- a/lib/ur/top.urs
+++ b/lib/ur/top.urs
@@ -290,3 +290,10 @@ val postFields : postBody -> list (string * string)
val max : t ::: Type -> ord t -> t -> t -> t
val min : t ::: Type -> ord t -> t -> t -> t
+
+val assert : t ::: Type
+ -> bool (* Did we avoid something bad? *)
+ -> string (* Explanation of the bad thing *)
+ -> string (* Source location of the bad thing *)
+ -> t (* Return this value if all went well. *)
+ -> t