Revert "fix(engine/fstar): fixes #719"

This reverts commit 6c77640.
hacspec · Jun 20, 2024 · 8dc62be · 8dc62be
1 parent 6c77640
commit 8dc62be
Show file tree

Hide file tree

Showing 10 changed files with 127 additions and 121 deletions.
diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml
@@ -458,7 +458,7 @@ struct
  |> List.map ~f:(function
  | GConst const -> (pexpr const, F.AST.Nothing)
  | GLifetime _ -> .
- | GType ty -> (pty e.span ty, F.AST.Nothing))
+ | GType ty -> (pty e.span ty, F.AST.Hash))
  in
  let args = List.map ~f:(pexpr &&& Fn.const F.AST.Nothing) args in
  F.mk_app (pexpr f) (generic_args @ args)
@@ -626,7 +626,7 @@ struct
  type kind = Implicit | Tcresolve | Explicit
  type t = { kind : kind; ident : F.Ident.ident; typ : F.AST.term }
 
- let of_generic_param ?(kind : kind = Explicit) span (p : generic_param) : t
+ let of_generic_param ?(kind : kind = Implicit) span (p : generic_param) : t
  =
  let ident = plocal_ident p.ident in
  match p.kind with
@@ -641,8 +641,8 @@ struct
  let typ = c_trait_goal span goal in
  { kind = Tcresolve; ident = F.id name; typ }
 
- let of_generics ?(kind : kind = Explicit) span generics : t list =
- List.map ~f:(of_generic_param ~kind:Explicit span) generics.params
+ let of_generics ?(kind : kind = Implicit) span generics : t list =
+ List.map ~f:(of_generic_param ~kind span) generics.params
  @ List.mapi ~f:(of_generic_constraint span) generics.constraints
 
  let of_typ span (nth : int) typ : t =
@@ -1166,7 +1166,7 @@ struct
  ~f:(fun i ->
  let name = U.Concrete_ident_view.to_definition_name i.ti_ident in
  let generics =
- FStarBinder.of_generics ~kind:Explicit i.ti_span i.ti_generics
+ FStarBinder.of_generics ~kind:Implicit i.ti_span i.ti_generics
  in
  let bds = generics |> List.map ~f:FStarBinder.to_binder in
  let fields =

diff --git a/test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap b/test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap
@@ -37,7 +37,7 @@ module Attribute_opaque
 open Core
 open FStar.Mul
 
-val t_OpaqueEnum (v_X: usize) (v_T v_U: Type0) : Type0
+val t_OpaqueEnum (v_X: usize) (#v_T #v_U: Type0) : Type0
 
-val t_OpaqueStruct (v_X: usize) (v_T v_U: Type0) : Type0
+val t_OpaqueStruct (v_X: usize) (#v_T #v_U: Type0) : Type0
 '''
diff --git a/test-harness/src/snapshots/toolchain__attributes into-fstar.snap b/test-harness/src/snapshots/toolchain__attributes into-fstar.snap
@@ -62,7 +62,7 @@ let impl__SafeIndex__new (i: usize) : Core.Option.t_Option t_SafeIndex =
  else Core.Option.Option_None <: Core.Option.t_Option t_SafeIndex
 
 [@@ FStar.Tactics.Typeclasses.tcinstance]
-let impl_1 (v_T: Type0) : Core.Ops.Index.t_Index (t_Array v_T (sz 10)) t_SafeIndex =
+let impl_1 (#v_T: Type0) : Core.Ops.Index.t_Index (t_Array v_T (sz 10)) t_SafeIndex =
  {
  f_Output = v_T;
  f_index_pre = (fun (self: t_Array v_T (sz 10)) (index: t_SafeIndex) -> true);
@@ -172,8 +172,8 @@ let t_NoE =
  x:
  Alloc.String.t_String
  { let _, out:(Core.Str.Iter.t_Chars & bool) =
- Core.Iter.Traits.Iterator.f_any Core.Str.Iter.t_Chars
- (Core.Str.impl__str__chars (Core.Ops.Deref.f_deref Alloc.String.t_String x <: string)
+ Core.Iter.Traits.Iterator.f_any #Core.Str.Iter.t_Chars
+ (Core.Str.impl__str__chars (Core.Ops.Deref.f_deref #Alloc.String.t_String x <: string)
  <:
  Core.Str.Iter.t_Chars)
  (fun ch ->
@@ -183,7 +183,8 @@ let t_NoE =
  ~.out }
 
 let bounded_u8 (x: t_BoundedU8 12uy 15uy) (y: t_BoundedU8 10uy 11uy) : t_BoundedU8 1uy 23uy =
- (Hax_lib.f_get (t_BoundedU8 12uy 15uy) x <: u8) +! (Hax_lib.f_get (t_BoundedU8 10uy 11uy) y <: u8)
+ (Hax_lib.f_get #(t_BoundedU8 12uy 15uy) x <: u8) +!
+ (Hax_lib.f_get #(t_BoundedU8 10uy 11uy) y <: u8)
  <:
  t_BoundedU8 1uy 23uy
 

diff --git a/test-harness/src/snapshots/toolchain__generics into-fstar.snap b/test-harness/src/snapshots/toolchain__generics into-fstar.snap
@@ -45,7 +45,7 @@ module Generics
 open Core
 open FStar.Mul
 
-let impl__Bar__inherent_impl_generics (v_T: Type0) (v_N: usize) (x: t_Array v_T v_N) : Prims.unit =
+let impl__Bar__inherent_impl_generics (#v_T: Type0) (v_N: usize) (x: t_Array v_T v_N) : Prims.unit =
  ()
 
 class t_Foo (v_Self: Type0) = {
@@ -63,23 +63,26 @@ let impl_Foo_for_usize: t_Foo usize =
  f_const_add = fun (v_N: usize) (self: usize) -> self +! v_N
  }
 
-let dup (v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Clone.t_Clone v_T) (x: v_T)
- : (v_T & v_T) = Core.Clone.f_clone v_T x, Core.Clone.f_clone v_T x <: (v_T & v_T)
+let dup
+ (#v_T: Type0)
+ (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Clone.t_Clone v_T)
+ (x: v_T)
+ : (v_T & v_T) = Core.Clone.f_clone #v_T x, Core.Clone.f_clone #v_T x <: (v_T & v_T)
 
 let f (v_N x: usize) : usize = (v_N +! v_N <: usize) +! x
 
 let call_f (_: Prims.unit) : usize = (f (sz 10) (sz 3) <: usize) +! sz 3
 
 let g
  (v_N: usize)
- (v_T: Type0)
+ (#v_T: Type0)
  (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Convert.t_Into v_T (t_Array usize v_N))
  (arr: v_T)
  : usize =
- (Core.Option.impl__unwrap_or usize
- (Core.Iter.Traits.Iterator.f_max (Core.Array.Iter.t_IntoIter usize v_N)
- (Core.Iter.Traits.Collect.f_into_iter (t_Array usize v_N)
- (Core.Convert.f_into v_T (t_Array usize v_N) arr <: t_Array usize v_N)
+ (Core.Option.impl__unwrap_or #usize
+ (Core.Iter.Traits.Iterator.f_max #(Core.Array.Iter.t_IntoIter usize v_N)
+ (Core.Iter.Traits.Collect.f_into_iter #(t_Array usize v_N)
+ (Core.Convert.f_into #v_T #(t_Array usize v_N) arr <: t_Array usize v_N)
  <:
  Core.Array.Iter.t_IntoIter usize v_N)
  <:
@@ -91,7 +94,7 @@ let g
 
 let call_g (_: Prims.unit) : usize =
  (g (sz 3)
- (t_Array usize (sz 3))
+ #(t_Array usize (sz 3))
  (let list = [sz 42; sz 3; sz 49] in
  FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 3);
  Rust_primitives.Hax.array_of_list 3 list)
@@ -102,7 +105,7 @@ let call_g (_: Prims.unit) : usize =
 let foo (v_LEN: usize) (arr: t_Array usize v_LEN) : usize =
  let acc:usize = v_LEN +! sz 9 in
  let acc:usize =
- Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Ops.Range.t_Range
+ Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Ops.Range.t_Range
  usize)
  ({ Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = v_LEN }
  <:
@@ -119,7 +122,7 @@ let foo (v_LEN: usize) (arr: t_Array usize v_LEN) : usize =
 
 let repeat
  (v_LEN: usize)
- (v_T: Type0)
+ (#v_T: Type0)
  (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Marker.t_Copy v_T)
  (x: v_T)
  : t_Array v_T v_LEN = Rust_primitives.Hax.repeat x v_LEN

diff --git a/test-harness/src/snapshots/toolchain__include-flag into-fstar.snap b/test-harness/src/snapshots/toolchain__include-flag into-fstar.snap
@@ -42,7 +42,7 @@ let main_a_b (_: Prims.unit) : Prims.unit = ()
 let main_a_c (_: Prims.unit) : Prims.unit = ()
 
 /// Direct dependencies
-let main_a (v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Trait v_T) (x: v_T)
+let main_a (#v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Trait v_T) (x: v_T)
  : Prims.unit =
  let _:Prims.unit = main_a_a () in
  let _:Prims.unit = main_a_b () in
@@ -80,7 +80,7 @@ let impl_Trait_for_Foo: t_Trait t_Foo = { __marker_trait = () }
 
 /// Entrypoint
 let main (_: Prims.unit) : Prims.unit =
- let _:Prims.unit = main_a t_Foo (Foo <: t_Foo) in
+ let _:Prims.unit = main_a #t_Foo (Foo <: t_Foo) in
  let _:Prims.unit = main_b () in
  let _:Prims.unit = main_c () in
  ()

diff --git a/test-harness/src/snapshots/toolchain__loops into-fstar.snap b/test-harness/src/snapshots/toolchain__loops into-fstar.snap
@@ -40,14 +40,14 @@ let bool_returning (x: u8) : bool = x <. 10uy
 let chunks (v_CHUNK_LEN: usize) (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize =
  let acc:usize = sz 0 in
  let chunks:Core.Slice.Iter.t_ChunksExact usize =
- Core.Slice.impl__chunks_exact usize
- (Core.Ops.Deref.f_deref (Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) arr <: t_Slice usize)
+ Core.Slice.impl__chunks_exact #usize
+ (Core.Ops.Deref.f_deref #(Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) arr <: t_Slice usize)
  v_CHUNK_LEN
  in
  let acc:usize =
- Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Slice.Iter.t_ChunksExact
+ Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Slice.Iter.t_ChunksExact
  usize)
- (Core.Clone.f_clone (Core.Slice.Iter.t_ChunksExact usize) chunks
+ (Core.Clone.f_clone #(Core.Slice.Iter.t_ChunksExact usize) chunks
  <:
  Core.Slice.Iter.t_ChunksExact usize)
  <:
@@ -58,7 +58,7 @@ let chunks (v_CHUNK_LEN: usize) (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global
  let chunk:t_Slice usize = chunk in
  let mean:usize = sz 0 in
  let mean:usize =
- Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (t_Slice usize)
+ Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(t_Slice usize)
  chunk
  <:
  Core.Slice.Iter.t_Iter usize)
@@ -72,8 +72,8 @@ let chunks (v_CHUNK_LEN: usize) (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global
  acc)
  in
  let acc:usize =
- Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (t_Slice usize)
- (Core.Slice.Iter.impl_87__remainder usize chunks <: t_Slice usize)
+ Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(t_Slice usize)
+ (Core.Slice.Iter.impl_87__remainder #usize chunks <: t_Slice usize)
  <:
  Core.Slice.Iter.t_Iter usize)
  acc
@@ -87,10 +87,10 @@ let chunks (v_CHUNK_LEN: usize) (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global
 let composed_range (n: usize) : usize =
  let acc:usize = sz 0 in
  let acc:usize =
- Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Iter.Adapters.Chain.t_Chain
+ Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Iter.Adapters.Chain.t_Chain
  (Core.Ops.Range.t_Range usize) (Core.Ops.Range.t_Range usize))
- (Core.Iter.Traits.Iterator.f_chain (Core.Ops.Range.t_Range usize)
- (Core.Ops.Range.t_Range usize)
+ (Core.Iter.Traits.Iterator.f_chain #(Core.Ops.Range.t_Range usize)
+ #(Core.Ops.Range.t_Range usize)
  ({ Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = n }
  <:
  Core.Ops.Range.t_Range usize)
@@ -117,11 +117,11 @@ let composed_range (n: usize) : usize =
 let enumerate_chunks (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize =
  let acc:usize = sz 0 in
  let acc:usize =
- Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Iter.Adapters.Enumerate.t_Enumerate
+ Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Iter.Adapters.Enumerate.t_Enumerate
  (Core.Slice.Iter.t_Chunks usize))
- (Core.Iter.Traits.Iterator.f_enumerate (Core.Slice.Iter.t_Chunks usize)
- (Core.Slice.impl__chunks usize
- (Core.Ops.Deref.f_deref (Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) arr
+ (Core.Iter.Traits.Iterator.f_enumerate #(Core.Slice.Iter.t_Chunks usize)
+ (Core.Slice.impl__chunks #usize
+ (Core.Ops.Deref.f_deref #(Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) arr
  <:
  t_Slice usize)
  (sz 4)
@@ -135,10 +135,10 @@ let enumerate_chunks (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize =
  (fun acc temp_1_ ->
  let acc:usize = acc in
  let i, chunk:(usize & t_Slice usize) = temp_1_ in
- Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Iter.Adapters.Enumerate.t_Enumerate
+ Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Iter.Adapters.Enumerate.t_Enumerate
  (Core.Slice.Iter.t_Iter usize))
- (Core.Iter.Traits.Iterator.f_enumerate (Core.Slice.Iter.t_Iter usize)
- (Core.Slice.impl__iter usize chunk <: Core.Slice.Iter.t_Iter usize)
+ (Core.Iter.Traits.Iterator.f_enumerate #(Core.Slice.Iter.t_Iter usize)
+ (Core.Slice.impl__iter #usize chunk <: Core.Slice.Iter.t_Iter usize)
  <:
  Core.Iter.Adapters.Enumerate.t_Enumerate (Core.Slice.Iter.t_Iter usize))
  <:
@@ -155,7 +155,8 @@ let enumerate_chunks (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize =
 
 let f (_: Prims.unit) : u8 =
  let acc:u8 = 0uy in
- Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Ops.Range.t_Range u8)
+ Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Ops.Range.t_Range u8
+ )
  ({ Core.Ops.Range.f_start = 1uy; Core.Ops.Range.f_end = 10uy } <: Core.Ops.Range.t_Range u8)
  <:
  Core.Ops.Range.t_Range u8)
@@ -170,10 +171,10 @@ let f (_: Prims.unit) : u8 =
 let iterator (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize =
  let acc:usize = sz 0 in
  let acc:usize =
- Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Slice.Iter.t_Iter
+ Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Slice.Iter.t_Iter
  usize)
- (Core.Slice.impl__iter usize
- (Core.Ops.Deref.f_deref (Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) arr
+ (Core.Slice.impl__iter #usize
+ (Core.Ops.Deref.f_deref #(Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) arr
  <:
  t_Slice usize)
  <:
@@ -191,10 +192,10 @@ let iterator (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize =
 let nested (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize =
  let acc:usize = sz 0 in
  let acc:usize =
- Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Slice.Iter.t_Iter
+ Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Slice.Iter.t_Iter
  usize)
- (Core.Slice.impl__iter usize
- (Core.Ops.Deref.f_deref (Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) arr
+ (Core.Slice.impl__iter #usize
+ (Core.Ops.Deref.f_deref #(Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) arr
  <:
  t_Slice usize)
  <:
@@ -205,9 +206,9 @@ let nested (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize =
  (fun acc item ->
  let acc:usize = acc in
  let item:usize = item in
- Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Iter.Adapters.Rev.t_Rev
+ Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Iter.Adapters.Rev.t_Rev
  (Core.Ops.Range.t_Range usize))
- (Core.Iter.Traits.Iterator.f_rev (Core.Ops.Range.t_Range usize)
+ (Core.Iter.Traits.Iterator.f_rev #(Core.Ops.Range.t_Range usize)
  ({ Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = item }
  <:
  Core.Ops.Range.t_Range usize)
@@ -220,12 +221,12 @@ let nested (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize =
  let acc:usize = acc in
  let i:usize = i in
  let acc:usize = acc +! sz 1 in
- Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Iter.Adapters.Zip.t_Zip
+ Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Iter.Adapters.Zip.t_Zip
  (Core.Slice.Iter.t_Iter usize) (Core.Ops.Range.t_Range usize))
- (Core.Iter.Traits.Iterator.f_zip (Core.Slice.Iter.t_Iter usize)
- (Core.Ops.Range.t_Range usize)
- (Core.Slice.impl__iter usize
- (Core.Ops.Deref.f_deref (Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global)
+ (Core.Iter.Traits.Iterator.f_zip #(Core.Slice.Iter.t_Iter usize)
+ #(Core.Ops.Range.t_Range usize)
+ (Core.Slice.impl__iter #usize
+ (Core.Ops.Deref.f_deref #(Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global)
  arr
  <:
  t_Slice usize)
@@ -253,7 +254,7 @@ let nested (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize =
 let pattern (arr: Alloc.Vec.t_Vec (usize & usize) Alloc.Alloc.t_Global) : usize =
  let acc:usize = sz 0 in
  let acc:usize =
- Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Alloc.Vec.t_Vec
+ Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Alloc.Vec.t_Vec
  (usize & usize) Alloc.Alloc.t_Global)
  arr
  <:
@@ -269,7 +270,7 @@ let pattern (arr: Alloc.Vec.t_Vec (usize & usize) Alloc.Alloc.t_Global) : usize
 let range1 (_: Prims.unit) : usize =
  let acc:usize = sz 0 in
  let acc:usize =
- Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Ops.Range.t_Range
+ Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Ops.Range.t_Range
  usize)
  ({ Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = sz 15 }
  <:
@@ -287,7 +288,7 @@ let range1 (_: Prims.unit) : usize =
 let range2 (n: usize) : usize =
  let acc:usize = sz 0 in
  let acc:usize =
- Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Ops.Range.t_Range
+ Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Ops.Range.t_Range
  usize)
  ({ Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = n +! sz 10 <: usize }
  <:
@@ -305,9 +306,9 @@ let range2 (n: usize) : usize =
 let rev_range (n: usize) : usize =
  let acc:usize = sz 0 in
  let acc:usize =
- Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Iter.Adapters.Rev.t_Rev
+ Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Iter.Adapters.Rev.t_Rev
  (Core.Ops.Range.t_Range usize))
- (Core.Iter.Traits.Iterator.f_rev (Core.Ops.Range.t_Range usize)
+ (Core.Iter.Traits.Iterator.f_rev #(Core.Ops.Range.t_Range usize)
  ({ Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = n }
  <:
  Core.Ops.Range.t_Range usize)