diff options
author | Son Ho | 2022-02-10 10:08:50 +0100 |
---|---|---|
committer | Son Ho | 2022-02-10 10:08:50 +0100 |
commit | 2a4aa027a496c95533f7970ff791420380e55e1f (patch) | |
tree | 43da03b893a7d703e031fba01514481d9abcb705 | |
parent | dcff2372f056af24c176b90797c10412b8b5f893 (diff) |
Improve slightly more the formatting
-rw-r--r-- | src/ExtractToFStar.ml | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml index def63db7..ccce4e1a 100644 --- a/src/ExtractToFStar.ml +++ b/src/ExtractToFStar.ml @@ -1033,13 +1033,16 @@ let extract_template_decreases_clause (ctx : extraction_ctx) (fmt : F.formatter) F.pp_print_string fmt ":"; F.pp_print_space fmt (); F.pp_print_string fmt "nat"; - (* Print the body *) + (* Print the "=" *) F.pp_print_space fmt (); F.pp_print_string fmt "="; - F.pp_print_space fmt (); - F.pp_print_string fmt "admit ()"; (* Close the box for "let FUN_NAME (PARAMS) =" *) F.pp_close_box fmt (); + (* Add a space before the "admit" and increment the indentation if we need + * to break line *) + F.pp_print_break fmt 1 ctx.indent_incr; + (* Print the "admit ()" *) + F.pp_print_string fmt "admit ()"; (* Close the box for the whole definition *) F.pp_close_box fmt (); (* Add breaks to insert new lines between definitions *) |