From e76ef95ddda11d4220e1f0fd863b0df568de95bc Mon Sep 17 00:00:00 2001
From: Aymeric Fromherz
Date: Thu, 23 May 2024 16:41:54 +0200
Subject: Add simp, reducible attributes to generated Lean projectors

---
 compiler/ExtractTypes.ml | 10 ++++++++++
 1 file changed, 10 insertions(+)

(limited to 'compiler')

diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml
index 8520b0fb..70a4d000 100644
--- a/compiler/ExtractTypes.ml
+++ b/compiler/ExtractTypes.ml
@@ -1701,6 +1701,16 @@ let extract_type_decl_lean_record_field_projectors (ctx : extraction_ctx)
           (* Inner box for the projector definition *)
           F.pp_open_hvbox fmt ctx.indent_incr;
 
+          (* Box for the attributes *)
+          F.pp_open_vbox fmt 0;
+          (* Annotate the projectors with both simp and reducible.
+             The first one allows to automatically unfold when calling simp in proofs.
+             The second ensures that projectors will interact well with the unifier *)
+          F.pp_print_string fmt "@[simp, reducible]";
+          F.pp_print_break fmt 0 0;
+          (* Close box for the attributes *)
+          F.pp_close_box fmt ();
+
           (* Box for the [def ADT.proj ... :=] *)
           F.pp_open_hovbox fmt ctx.indent_incr;
           F.pp_print_string fmt "def";
-- 
cgit v1.2.3