diff --git a/test-harness/src/snapshots/toolchain__traits into-fstar.snap b/test-harness/src/snapshots/toolchain__traits into-fstar.snap index ed926974c..aab9040a4 100644 --- a/test-harness/src/snapshots/toolchain__traits into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__traits into-fstar.snap @@ -58,6 +58,29 @@ class t_Foo (v_Self: Type) = { f_method_f:v_Self -> Prims.unit } +let closure_impl_expr + (#v_I: Type) + (#[FStar.Tactics.Typeclasses.tcresolve ()] i0: Core.Marker.t_Sized v_I) + (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Iter.Traits.Iterator.t_Iterator v_I) + (it: v_I) + : Alloc.Vec.t_Vec Prims.unit Alloc.Alloc.t_Global = + Core.Iter.Traits.Iterator.f_collect (Core.Iter.Traits.Iterator.f_map it (fun x -> x) + <: + Core.Iter.Adapters.Map.t_Map v_I (Prims.unit -> Prims.unit)) + +let closure_impl_expr_fngen + (#v_I #v_F: Type) + (#[FStar.Tactics.Typeclasses.tcresolve ()] i0: Core.Marker.t_Sized v_I) + (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Marker.t_Sized v_F) + (#[FStar.Tactics.Typeclasses.tcresolve ()] i2: Core.Iter.Traits.Iterator.t_Iterator v_I) + (#[FStar.Tactics.Typeclasses.tcresolve ()] i3: Core.Ops.Function.t_FnMut v_F Prims.unit) + (it: v_I) + (f: v_F) + : Alloc.Vec.t_Vec Prims.unit Alloc.Alloc.t_Global = + Core.Iter.Traits.Iterator.f_collect (Core.Iter.Traits.Iterator.f_map it f + <: + Core.Iter.Adapters.Map.t_Map v_I v_F) + let f (#v_T: Type) (#[FStar.Tactics.Typeclasses.tcresolve ()] i0: Core.Marker.t_Sized v_T) diff --git a/tests/traits/src/lib.rs b/tests/traits/src/lib.rs index 6b993a484..f0238d71c 100644 --- a/tests/traits/src/lib.rs +++ b/tests/traits/src/lib.rs @@ -48,3 +48,11 @@ impl<'a> Struct { x.bar() } } + +pub fn closure_impl_expr>(it: I) -> Vec<()> { + it.map(|x| x).collect() +} + +pub fn closure_impl_expr_fngen, F: FnMut(()) -> ()>(it: I, f: F) -> Vec<()> { + it.map(f).collect() +}