diff options
author | Son Ho | 2022-02-02 17:13:07 +0100 |
---|---|---|
committer | Son Ho | 2022-02-02 17:13:07 +0100 |
commit | 6ee61aa87a564768d954ad767673b2b25a340516 (patch) | |
tree | 8f21e845a96cf838bddf4394d196cd43b73bf6d5 /src | |
parent | 7e87e22c3b739583b695d9c46ac44e00e941f9b7 (diff) |
Update a comment
Diffstat (limited to 'src')
-rw-r--r-- | src/ExtractToFStar.ml | 12 |
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") |