summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorSon Ho2022-02-02 17:13:07 +0100
committerSon Ho2022-02-02 17:13:07 +0100
commit6ee61aa87a564768d954ad767673b2b25a340516 (patch)
tree8f21e845a96cf838bddf4394d196cd43b73bf6d5 /src
parent7e87e22c3b739583b695d9c46ac44e00e941f9b7 (diff)
Update a comment
Diffstat (limited to 'src')
-rw-r--r--src/ExtractToFStar.ml12
1 files changed, 10 insertions, 2 deletions
diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml
index 6fd141cc..26316bc4 100644
--- a/src/ExtractToFStar.ml
+++ b/src/ExtractToFStar.ml
@@ -203,7 +203,15 @@ let extract_type_def_struct_body (ctx : extraction_ctx) (fmt : F.formatter)
* type t = { x : int; y : bool; }
* ```
*
- * Or if there isn't enough space on one line:
+ * If there isn't enough space on one line:
+ * ```
+ * type t =
+ * {
+ * x : int; y : bool;
+ * }
+ * ```
+ *
+ * And if there is even less space:
* ```
* type t =
* {
@@ -211,11 +219,11 @@ let extract_type_def_struct_body (ctx : extraction_ctx) (fmt : F.formatter)
* y : bool;
* }
* ```
- * Note that we already printed: `type t =`
*
* Also, in case there are no fields, we need to define the type as `unit`
* (`type t = {}` doesn't work in F* ).
*)
+ (* Note that we already printed: `type t =` *)
if fields = [] then (
F.pp_print_space fmt ();
F.pp_print_string fmt "unit")