diff options
Diffstat (limited to 'compiler/Extract.ml')
| -rw-r--r-- | compiler/Extract.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/compiler/Extract.ml b/compiler/Extract.ml index 4acf3f99..b1adb936 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -1448,6 +1448,10 @@ let extract_fun_decl_gen (ctx : extraction_ctx) (fmt : F.formatter) (* Open two boxes for the definition, so that whenever possible it gets printed on * one line and indents are correct *) F.pp_open_hvbox fmt 0; + (* Print the attributes *) + if def.backend_attributes.reducible && backend () = Lean then ( + F.pp_print_string fmt "@[reducible]"; + F.pp_print_space fmt ()); F.pp_open_vbox fmt ctx.indent_incr; (* For HOL4: we may need to put parentheses around the definition *) let parenthesize = backend () = HOL4 && decl_is_not_last_from_group kind in |