5 files changed, 30 insertions, 1 deletions
diff --git a/lib/flow.sail b/lib/flow.sail
index b4440eaa..c16763ee 100644
--- a/lib/flow.sail
+++ b/lib/flow.sail
@@ -1,6 +1,10 @@
 $ifndef _FLOW
 $define _FLOW
 
+val eq_unit : (unit, unit) -> bool
+
+function eq_unit(_, _) = true
+
 val not_bool = {coq: "negb", _: "not"} : bool -> bool
 /* NB: There are special cases in Sail for effectful uses of and_bool and
    or_bool that are not shown here. */
@@ -45,7 +49,7 @@ val gteq_int = {coq: "Z.geb", _:"gteq"} : (int, int) -> bool
 val lt_int = {coq: "Z.ltb", _:"lt"} : (int, int) -> bool
 val gt_int = {coq: "Z.gtb", _:"gt"} : (int, int) -> bool
 
-overload operator == = {eq_atom, eq_range, eq_int, eq_bool}
+overload operator == = {eq_atom, eq_range, eq_int, eq_bool, eq_unit}
 overload operator != = {neq_atom, neq_range, neq_int, neq_bool}
 overload operator | = {or_bool}
 overload operator & = {and_bool}
diff --git a/test/c/mapping.expect b/test/c/mapping.expect
new file mode 100644
index 00000000..49f4aaa8
--- /dev/null
+++ b/test/c/mapping.expect
@@ -0,0 +1 @@
+m() = 1
diff --git a/test/c/mapping.sail b/test/c/mapping.sail
new file mode 100644
index 00000000..3d232a42
--- /dev/null
+++ b/test/c/mapping.sail
@@ -0,0 +1,17 @@
+default Order dec
+
+$include <flow.sail>
+$include <arith.sail>
+
+val m : unit <-> int(1)
+
+mapping m = {
+  () <-> 1
+}
+
+val main : unit -> unit
+
+function main() = {
+  print_int("m() = ", m());
+  m(1)
+}
+\ No newline at end of file
diff --git a/test/c/prelude.expect b/test/c/prelude.expect
new file mode 100644
index 00000000..e69de29b
--- /dev/null
+++ b/test/c/prelude.expect
diff --git a/test/c/prelude.sail b/test/c/prelude.sail
new file mode 100644
index 00000000..7e217f5d
--- /dev/null
+++ b/test/c/prelude.sail
@@ -0,0 +1,7 @@
+default Order dec
+
+$include <prelude.sail>
+
+val main : unit -> unit
+
+function main() = ()