From f4739fba4be95818ca01776837c8d610e443a45b Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 17 Jun 2024 07:14:52 +0200
Subject: Automatically add a @[reducible] attribute to some generated
 functions

---
 compiler/Extract.ml | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'compiler/Extract.ml')

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
-- 
cgit v1.2.3