summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGabriel Kerneis2014-02-18 17:02:13 +0000
committerGabriel Kerneis2014-02-18 17:02:13 +0000
commit02b78a552d92582b54c78560c791bad4f1532fc1 (patch)
treeaad82a1b125b3c1a8cdf6ca5c71f2003d134057b
parent669ced036bc511f6c75b91a9abb3dd3f607cf0a1 (diff)
Remove spurious add infix
-rw-r--r--src/lem_interp/interp_lib.lem1
-rw-r--r--src/test/test3.sail2
2 files changed, 1 insertions, 2 deletions
diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem
index d1703502..aeb81085 100644
--- a/src/lem_interp/interp_lib.lem
+++ b/src/lem_interp/interp_lib.lem
@@ -68,7 +68,6 @@ let rec vec_concat (V_tuple args) = match args with
let function_map = [
("add", add);
- ("add_infix", add);
("eq", eq);
("vec_concat", vec_concat);
("is_one", is_one);
diff --git a/src/test/test3.sail b/src/test/test3.sail
index ed30d243..b07ffb7d 100644
--- a/src/test/test3.sail
+++ b/src/test/test3.sail
@@ -17,7 +17,7 @@ function unit ignore(x) = ()
(* extern functions *)
val extern ( nat * nat ) -> nat effect pure add = "add"
-val extern ( nat * nat ) -> nat effect pure (deinfix + ) = "add_infix" (* infix plus *)
+val extern ( nat * nat ) -> nat effect pure (deinfix + ) = "add" (* infix plus *)
function nat (deinfix * ) ( (nat) x, (nat) y ) = 42