From 7238177f5c7cff15f924e13c01d5b3b4802daf77 Mon Sep 17 00:00:00 2001
From: Aymeric Fromherz
Date: Thu, 23 May 2024 11:33:46 +0200
Subject: Do not expand field projector for recursive structs to a let binding
 in Lean

---
 compiler/SymbolicToPure.ml | 5 -----
 1 file changed, 5 deletions(-)

(limited to 'compiler')

diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 6c925bcd..351f5cf2 100644
--- 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
-- 
cgit v1.2.3