summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2008-08-31 15:18:00 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2008-08-31 15:18:00 -0400
commit959f07d717b29f083b275333b38e40e5b9f78a9d (patch)
tree12350e6dcc8fba4e292634d86afb756bf466b210
parent6a144b5f5a7e85a02465aa25a19c3b5686e062cb (diff)
Add 'ne' to 'eq' type class
-rw-r--r--lib/basis.urs2
-rw-r--r--src/urweb.grm1
-rw-r--r--tests/eq.ur2
3 files changed, 4 insertions, 1 deletions
diff --git a/lib/basis.urs b/lib/basis.urs
index bc4c9481..c83ec044 100644
--- a/lib/basis.urs
+++ b/lib/basis.urs
@@ -11,8 +11,8 @@ datatype bool = False | True
class eq
val eq : t ::: Type -> eq t -> t -> t -> bool
+val ne : t ::: Type -> eq t -> t -> t -> bool
val eq_int : eq int
-val eq_float : eq float
val eq_string : eq string
val eq_bool : eq bool
diff --git a/src/urweb.grm b/src/urweb.grm
index 9d619fca..51c104d7 100644
--- a/src/urweb.grm
+++ b/src/urweb.grm
@@ -605,6 +605,7 @@ eexp : eapps (eapps)
(EApp (e, (EAbs (SYMBOL, NONE, eexp2), loc)), loc)
end)
| eexp EQ eexp (native_op ("eq", eexp1, eexp2, s (eexp1left, eexp2right)))
+ | eexp NE eexp (native_op ("ne", eexp1, eexp2, s (eexp1left, eexp2right)))
eargs : earg (earg)
| eargl (eargl)
diff --git a/tests/eq.ur b/tests/eq.ur
index 0c5cde60..14c50e3a 100644
--- a/tests/eq.ur
+++ b/tests/eq.ur
@@ -3,3 +3,5 @@ val b2 = "Good" = "Bad"
fun eq_pair (t1 :: Type) (t2 :: Type) (eq1 : eq t1) (eq2 : eq t2) (x : t1 * t2) (y : t1 * t2) =
x.1 = y.1
+
+val b3 = True <> False