feat(lean): associated types with equality constraints

CHANGELOG.md

@@ -37,6 +37,7 @@ Changes to the Lean backend:
  - Add support for binding subpatterns in match constructs (#1790)
  - Add error when using patterns in function parameters (#1792)
  - Add support for constant parameters to functions and traits (#1797)
+ - Add support for associated types with equality constraints (#1806)
 
 Miscellaneous:
 - Reserve extraction folder for auto-generated files in Lean examples (#1754)

rust-engine/src/ast.rs

@@ -1452,6 +1452,23 @@ pub struct Module {
     pub meta: Metadata,
 }
 
+impl Generics {
+    /// Returns Iterator over all type constraints (`GenericConstraint::Type`)
+    pub fn type_constraints(&self) -> impl Iterator<Item = &ImplIdent> {
+        self.constraints.iter().filter_map(|c| match c {
+            GenericConstraint::Type(impl_id) => Some(impl_id),
+            _ => None,
+        })
+    }
+    /// Returns Iterator over all projection constraints (`GenericConstraint::Projection`)
+    pub fn projection_constraints(&self) -> impl Iterator<Item = &ProjectionPredicate> {
+        self.constraints.iter().filter_map(|c| match c {
+            GenericConstraint::Projection(pp) => Some(pp),
+            _ => None,
+        })
+    }
+}
+
 /// Traits for utilities on AST data types
 pub mod traits {
     use super::*;

test-harness/src/snapshots/toolchain__lean-core-models into-lean.snap

@@ -46,11 +46,14 @@ inductive Lean_core_models.Result.E1 : Type
 | C2 : u32 -> Lean_core_models.Result.E1
 
 
+instance Lean_core_models.Result.Impl.AssociatedTypes :
+  Core.Clone.Clone.AssociatedTypes Lean_core_models.Result.E1
+  where
+
 instance Lean_core_models.Result.Impl :
   Core.Clone.Clone Lean_core_models.Result.E1
   where
 
-
 inductive Lean_core_models.Result.E2 : Type
 | C1 : Lean_core_models.Result.E2
 | C2 : u32 -> Lean_core_models.Result.E2
@@ -142,6 +145,10 @@ inductive Lean_core_models.Option.E : Type
 | C : u32 -> Lean_core_models.Option.E
 
 
+instance Lean_core_models.Option.Impl.AssociatedTypes :
+  Core.Default.Default.AssociatedTypes Lean_core_models.Option.S
+  where
+
 instance Lean_core_models.Option.Impl :
   Core.Default.Default Lean_core_models.Option.S
   where
@@ -235,6 +242,10 @@ def Lean_core_models.Option.test
 structure Lean_core_models.Default.Structs.S where
   f1 : usize
 
+instance Lean_core_models.Default.Structs.Impl.AssociatedTypes :
+  Core.Default.Default.AssociatedTypes Lean_core_models.Default.Structs.S
+  where
+
 instance Lean_core_models.Default.Structs.Impl :
   Core.Default.Default Lean_core_models.Default.Structs.S
   where
@@ -252,8 +263,17 @@ inductive Lean_core_models.Default.Enums.E (T : Type) : Type
 | C2 : T -> Lean_core_models.Default.Enums.E (T : Type) 
 
 
+instance Lean_core_models.Default.Enums.Impl.AssociatedTypes
+  (T : Type)
+  [Core.Default.Default.AssociatedTypes T] [Core.Default.Default T ]
+  :
+  Core.Default.Default.AssociatedTypes (Lean_core_models.Default.Enums.E T)
+  where
+
 instance Lean_core_models.Default.Enums.Impl
-  (T : Type) [(Core.Default.Default T)] :
+  (T : Type)
+  [Core.Default.Default.AssociatedTypes T] [Core.Default.Default T ]
+  :
   Core.Default.Default (Lean_core_models.Default.Enums.E T)
   where
   default (_ : Rust_primitives.Hax.Tuple0) := do