diff options
author | Adam Chlipala <adamc@hcoop.net> | 2008-08-31 15:18:00 -0400 |
---|---|---|
committer | Adam Chlipala <adamc@hcoop.net> | 2008-08-31 15:18:00 -0400 |
commit | 959f07d717b29f083b275333b38e40e5b9f78a9d (patch) | |
tree | 12350e6dcc8fba4e292634d86afb756bf466b210 | |
parent | 6a144b5f5a7e85a02465aa25a19c3b5686e062cb (diff) |
Add 'ne' to 'eq' type class
-rw-r--r-- | lib/basis.urs | 2 | ||||
-rw-r--r-- | src/urweb.grm | 1 | ||||
-rw-r--r-- | tests/eq.ur | 2 |
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 |