diff options
author | Aymeric Fromherz | 2024-05-23 16:41:54 +0200 |
---|---|---|
committer | Aymeric Fromherz | 2024-05-23 16:41:57 +0200 |
commit | e76ef95ddda11d4220e1f0fd863b0df568de95bc (patch) | |
tree | 09c091babfa10448192afd24c92805c7e964369e /compiler | |
parent | b4cc9c908935eb95c761b664e75ce065fb97d85c (diff) |
Add simp, reducible attributes to generated Lean projectors
Diffstat (limited to '')
-rw-r--r-- | compiler/ExtractTypes.ml | 10 |
1 files changed, 10 insertions, 0 deletions
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"; |