fixed Bool printing

rems-project · Nov 25, 2024 · 44e3256 · 44e3256
1 parent 9abdddc
commit 44e3256
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 1 deletion.
diff --git a/lib/vector.sail b/lib/vector.sail
@@ -60,6 +60,7 @@ val eq_bits = pure {
   interpreter: "eq_list",
   lem: "eq_vec",
   coq: "eq_vec",
+  lean: "Eq",
   _: "eq_bits"
 } : forall 'n. (bits('n), bits('n)) -> bool
 
@@ -68,7 +69,8 @@ overload operator == = {eq_bit, eq_bits}
 val neq_bits = pure {
   lem: "neq_vec",
   coq: "neq_vec",
-  c: "neq_bits"
+  c: "neq_bits",
+  lean: "Ne"
 } : forall 'n. (bits('n), bits('n)) -> bool
 
 function neq_bits(x, y) = not_bool(eq_bits(x, y))

diff --git a/src/sail_lean_backend/pretty_print_lean.ml b/src/sail_lean_backend/pretty_print_lean.ml
@@ -74,6 +74,7 @@ let rec doc_typ (Typ_aux (t, _) as typ) =
   match t with
   | Typ_id (Id_aux (Id "unit", _)) -> string "Unit"
   | Typ_id (Id_aux (Id "int", _)) -> string "Int"
+  | Typ_id (Id_aux (Id "bool", _)) -> string "Bool"
   | Typ_app (Id_aux (Id "bitvector", _), [A_aux (A_nexp m, _)]) -> string "BitVec " ^^ doc_nexp m
   | Typ_tuple ts -> parens (separate_map (space ^^ string "×" ^^ space) doc_typ ts)
   | Typ_id (Id_aux (Id id, _)) -> string id