2 files changed, 22 insertions, 10 deletions
diff --git a/src/gen_lib/sail2_values.lem b/src/gen_lib/sail2_values.lem
index 7bd950d7..9e1f20c0 100644
--- a/src/gen_lib/sail2_values.lem
+++ b/src/gen_lib/sail2_values.lem
@@ -35,15 +35,27 @@ let power_int_nat l r = integerPow l r
 let power_int_int l r = integerPow l (nat_of_int r)
 let negate_int i = integerNegate i
 let min_int l r = integerMin l r
-let max_int l r = integerMax l r
-
-let add_real l r = realAdd l r
-let sub_real l r = realMinus l r
-let mult_real l r = realMult l r
-let div_real l r = realDiv l r
-let negate_real r = realNegate r
-let abs_real r = realAbs r
-let power_real b e = realPowInteger b e*)
+let max_int l r = integerMax l r*)
+
+let inline add_real l r = realAdd l r
+let inline sub_real l r = realMinus l r
+let inline mult_real l r = realMult l r
+let inline div_real l r = realDiv l r
+let inline neg_real r = realNegate r
+let inline abs_real r = realAbs r
+let inline real_power b e = realPowInteger b e
+let inline sqrt_real r = realSqrt r
+
+let inline eq_real l r = realEq l r
+let inline lt_real l r = realLess l r
+let inline gt_real l r = realLessEqual l r
+let inline lteq_real l r = realGreater l r
+let inline gteq_real l r = realGreaterEqual l r
+
+let inline to_real i = realFromInteger i
+
+let inline round_down r = realFloor r
+let inline round_up r = realCeiling r
 
 val print_endline : string -> unit
 let print_endline _ = ()
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index 993934f5..34ccc5ba 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -901,7 +901,7 @@ let doc_exp_lem, doc_let_lem =
            when Env.is_record tid env ->
            tid
          | _ ->  raise (report l __POS__ ("cannot get record type from annot " ^ string_of_tannot annot ^ " of exp " ^ string_of_exp full_exp)) in
-       anglebars (doc_op (string "with") (expY e) (separate_map semi_sp (doc_fexp ctxt recordtyp) fexps))
+       anglebars (space ^^ doc_op (string "with") (expY e) (separate_map semi_sp (doc_fexp ctxt recordtyp) fexps)  ^^ space)
     | E_vector exps ->
        let t = Env.base_typ_of (env_of full_exp) (typ_of full_exp) in
        let start, (len, order, etyp) =