Do not expand field projector for recursive structs to a let binding …

…in Lean
AeneasVerif · May 23, 2024 · 656150e · 656150e
1 parent c458a34
commit 656150e
Showing 1 changed file with 0 additions and 5 deletions.
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
@@ -2902,14 +2902,9 @@ and translate_ExpandAdt_one_branch (sv : V.symbolic_value)
          - if the ADT is an enumeration (which must have exactly one branch)
          - if we forbid using field projectors.
       *)
-      let is_rec_def =
-        T.TypeDeclId.Set.mem adt_id ctx.type_ctx.recursive_decls
-      in
       let use_let_with_cons =
         is_enum
         || !Config.dont_use_field_projectors
-        (* TODO: for now, we don't have field projectors over recursive ADTs in Lean. *)
-        || (!Config.backend = Lean && is_rec_def)
         (* Also, there is a special case when the ADT is to be extracted as
            a tuple, because it is a structure with unnamed fields. Some backends
            like Lean have projectors for tuples (like so: `x.3`), but others