File tree Expand file tree Collapse file tree 3 files changed +4
-4
lines changed
coq/coq/generated-core/src Expand file tree Collapse file tree 3 files changed +4
-4
lines changed Original file line number Diff line number Diff line change @@ -100,15 +100,15 @@ Instance t_RangeIteratorImpl_158276838 `{v_A : Type} `{t_Sized (v_A)} `{t_Step (
100
100
{
101
101
RangeIteratorImpl_impl_f_Item := v_A;
102
102
RangeIteratorImpl_impl_f_spec_next := fun (self : t_Range ((v_A)))=>
103
- let hax_temp_output := never_to_any (panic_fmt (impl_2__new_v1 (["not yet implemented: specification needed"%string]) (impl_1__none (tt)))) in
103
+ let hax_temp_output := never_to_any (panic_fmt (impl_1__new_v1 (["not yet implemented: specification needed"%string]) (impl_1__none (tt)))) in
104
104
(self,hax_temp_output);
105
105
}.
106
106
107
107
Instance t_Iterator_416192239 `{v_A : Type } `{t_Sized (v_A)} `{t_Step (v_A)} : t_Iterator ((t_Range ((v_A)))) :=
108
108
{
109
109
Iterator_impl_1_f_Item := v_A;
110
110
Iterator_impl_1_f_next := fun (self : t_Range ((v_A)))=>
111
- let hax_temp_output := never_to_any (panic_fmt (impl_2__new_v1 (["not yet implemented: specification needed"%string]) (impl_1__none (tt)))) in
111
+ let hax_temp_output := never_to_any (panic_fmt (impl_1__new_v1 (["not yet implemented: specification needed"%string]) (impl_1__none (tt)))) in
112
112
(self,hax_temp_output);
113
113
Iterator_impl_1_f_size_hint := fun (self : t_Range ((v_A)))=>
114
114
if
Original file line number Diff line number Diff line change @@ -3,7 +3,7 @@ open Rust_primitives
3
3
4
4
include Core.Fmt
5
5
6
- val impl_2__new_v1 ( sz1 : usize ) ( sz2 : usize ) ( pieces : t_Slice string) ( args : Core.Fmt.Rt. t_Argument ): t_Arguments
6
+ val impl_1__new_v1 ( sz1 : usize ) ( sz2 : usize ) ( pieces : t_Slice string) ( args : Core.Fmt.Rt. t_Argument ): t_Arguments
7
7
val impl_7__write_fmt ( fmt : t_Formatter ) ( args : t_Arguments ): t_Result
8
8
9
9
val format ( args : t_Arguments ): string
Original file line number Diff line number Diff line change @@ -8,7 +8,7 @@ val impl_4__new_v1_formatted (#t:Type0) (x: t) : t_Argument
8
8
val impl_1__new_binary (# t :Type0) ( x : t ) : t_Argument
9
9
val impl_1__new_lower_hex (# t :Type0) ( x : t ) : t_Argument
10
10
val impl_2__new_const (# t :Type0) (# u :Type0) ( xconst : t ) ( yconst : u ): t_Argument
11
- val impl_2__new_v1 (# t1 :Type0) (# t2 :Type0) (# t3 :Type0) (# t4 :Type0)
11
+ val impl_1__new_v1 (# t1 :Type0) (# t2 :Type0) (# t3 :Type0) (# t4 :Type0)
12
12
( x1 : t1 ) ( x2 : t2 ) ( x3 : t3 ) ( x4 : t4 ) : t_Argument
13
13
val impl__new_display (# t :Type0) ( x : t ): t_Argument
14
14
val impl__new_debug (# t :Type0) ( x : t ): t_Argument
You can’t perform that action at this time.
0 commit comments