summaryrefslogtreecommitdiff
path: root/lib/ur/top.urs
diff options
context:
space:
mode:
authorGravatar Benjamin Barenblat <bbaren@mit.edu>2015-08-19 11:02:23 -0400
committerGravatar Benjamin Barenblat <bbaren@mit.edu>2015-08-19 11:02:23 -0400
commit598756dc69f89cf2dd2b889cad63a7a690ae7ed7 (patch)
tree5fc521225e717163c30ea494a5839c26725eec2e /lib/ur/top.urs
parent7ea9d17bad72cf2829c75d8d241fafa70b2c9b94 (diff)
parentfb6e6599b35df9cfa05786772868b1a3d2e58ac3 (diff)
Merge branch 'upstream' into dfsg_clean20150819+dfsg
Conflicts: doc/intro.ur
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