From 6ee61aa87a564768d954ad767673b2b25a340516 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 2 Feb 2022 17:13:07 +0100 Subject: Update a comment --- src/ExtractToFStar.ml | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) (limited to 'src/ExtractToFStar.ml') 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") -- cgit v1.2.3