dafny_runtime/system/
mod.rs

1#![allow(warnings, unconditional_panic)]
2#![allow(nonstandard_style)]
3#![cfg_attr(any(), rustfmt::skip)]
4
5pub mod _System {
6    pub use crate::DafnyInt;
7    pub use crate::DafnyType;
8    pub use ::std::fmt::Debug;
9    pub use ::std::fmt::Formatter;
10    pub use ::std::fmt::Result;
11    pub use crate::DafnyPrint;
12    #[cfg(feature = "sync")] pub use ::std::sync::{Arc as Rc}; #[cfg(not(feature = "sync"))] pub use ::std::rc::Rc;
13    pub use ::std::cmp::Eq;
14    pub use ::std::hash::Hash;
15    pub use ::std::cmp::PartialEq;
16    pub use ::std::hash::Hasher;
17    pub use ::std::convert::AsRef;
18    pub use crate::SequenceIter;
19    pub use crate::seq;
20
21    pub type nat = DafnyInt;
22
23    #[derive(Clone)]
24    pub enum Tuple2<T0: DafnyType, T1: DafnyType> {
25        _T2 {
26            _0: T0,
27            _1: T1
28        }
29    }
30
31    impl<T0: DafnyType, T1: DafnyType> Tuple2<T0, T1> {
32        /// Returns a borrow of the field _0
33        pub fn _0(&self) -> &T0 {
34            match self {
35                Tuple2::_T2{_0, _1, } => _0,
36            }
37        }
38        /// Returns a borrow of the field _1
39        pub fn _1(&self) -> &T1 {
40            match self {
41                Tuple2::_T2{_0, _1, } => _1,
42            }
43        }
44    }
45
46    impl<T0: DafnyType, T1: DafnyType> Debug
47        for Tuple2<T0, T1> {
48        fn fmt(&self, f: &mut Formatter) -> Result {
49            DafnyPrint::fmt_print(self, f, true)
50        }
51    }
52
53    impl<T0: DafnyType, T1: DafnyType> DafnyPrint
54        for Tuple2<T0, T1> {
55        fn fmt_print(&self, _formatter: &mut Formatter, _in_seq: bool) -> std::fmt::Result {
56            match self {
57                Tuple2::_T2{_0, _1, } => {
58                    write!(_formatter, "(")?;
59                    DafnyPrint::fmt_print(_0, _formatter, false)?;
60                    write!(_formatter, ", ")?;
61                    DafnyPrint::fmt_print(_1, _formatter, false)?;
62                    write!(_formatter, ")")?;
63                    Ok(())
64                },
65            }
66        }
67    }
68
69    impl<T0: DafnyType, T1: DafnyType> Tuple2<T0, T1> {
70        /// Given type parameter conversions, returns a lambda to convert this structure
71        pub fn coerce<__T0: DafnyType, __T1: DafnyType>(f_0: Rc<impl ::std::ops::Fn(T0) -> __T0 + 'static>, f_1: Rc<impl ::std::ops::Fn(T1) -> __T1 + 'static>) -> Rc<impl ::std::ops::Fn(Tuple2<T0, T1>) -> Tuple2<__T0, __T1>> {
72            Rc::new(move |this: Self| -> Tuple2<__T0, __T1>{
73                    match this {
74                        Tuple2::_T2{_0, _1, } => {
75                            Tuple2::_T2 {
76                                _0: f_0.clone()(_0),
77                                _1: f_1.clone()(_1)
78                            }
79                        },
80                    }
81                })
82        }
83    }
84
85    impl<T0: DafnyType + Eq + Hash, T1: DafnyType + Eq + Hash> PartialEq
86        for Tuple2<T0, T1> {
87        fn eq(&self, other: &Self) -> bool {
88            match (
89                    self,
90                    other
91                ) {
92                (Tuple2::_T2{_0, _1, }, Tuple2::_T2{_0: _2__0, _1: _2__1, }) => {
93                    _0 == _2__0 && _1 == _2__1
94                },
95                _ => {
96                    false
97                },
98            }
99        }
100    }
101
102    impl<T0: DafnyType + Eq + Hash, T1: DafnyType + Eq + Hash> Eq
103        for Tuple2<T0, T1> {}
104
105    impl<T0: DafnyType + Hash, T1: DafnyType + Hash> Hash
106        for Tuple2<T0, T1> {
107        fn hash<_H: Hasher>(&self, _state: &mut _H) {
108            match self {
109                Tuple2::_T2{_0, _1, } => {
110                    Hash::hash(_0, _state);
111                    Hash::hash(_1, _state)
112                },
113            }
114        }
115    }
116
117    impl<T0: DafnyType, T1: DafnyType> AsRef<Tuple2<T0, T1>>
118        for Tuple2<T0, T1> {
119        fn as_ref(&self) -> &Self {
120            self
121        }
122    }
123
124    #[derive(Clone)]
125    pub enum Tuple0 {
126        _T0 {}
127    }
128
129    impl Tuple0 {}
130
131    impl Debug
132        for Tuple0 {
133        fn fmt(&self, f: &mut Formatter) -> Result {
134            DafnyPrint::fmt_print(self, f, true)
135        }
136    }
137
138    impl DafnyPrint
139        for Tuple0 {
140        fn fmt_print(&self, _formatter: &mut Formatter, _in_seq: bool) -> std::fmt::Result {
141            match self {
142                Tuple0::_T0{} => {
143                    write!(_formatter, "")?;
144                    Ok(())
145                },
146            }
147        }
148    }
149
150    impl Tuple0 {
151        /// Enumerates all possible values of Tuple0
152        pub fn _AllSingletonConstructors() -> SequenceIter<Rc<Tuple0>> {
153            seq![Rc::new(Tuple0::_T0 {})].iter()
154        }
155    }
156
157    impl PartialEq
158        for Tuple0 {
159        fn eq(&self, other: &Self) -> bool {
160            match (
161                    self,
162                    other
163                ) {
164                (Tuple0::_T0{}, Tuple0::_T0{}) => {
165                    true
166                },
167                _ => {
168                    false
169                },
170            }
171        }
172    }
173
174    impl Eq
175        for Tuple0 {}
176
177    impl Hash
178        for Tuple0 {
179        fn hash<_H: Hasher>(&self, _state: &mut _H) {
180            match self {
181                Tuple0::_T0{} => {
182                    
183                },
184            }
185        }
186    }
187
188    impl AsRef<Tuple0>
189        for Tuple0 {
190        fn as_ref(&self) -> &Self {
191            self
192        }
193    }
194
195    #[derive(Clone)]
196    pub enum Tuple1<T0: DafnyType> {
197        _T1 {
198            _0: T0
199        }
200    }
201
202    impl<T0: DafnyType> Tuple1<T0> {
203        /// Returns a borrow of the field _0
204        pub fn _0(&self) -> &T0 {
205            match self {
206                Tuple1::_T1{_0, } => _0,
207            }
208        }
209    }
210
211    impl<T0: DafnyType> Debug
212        for Tuple1<T0> {
213        fn fmt(&self, f: &mut Formatter) -> Result {
214            DafnyPrint::fmt_print(self, f, true)
215        }
216    }
217
218    impl<T0: DafnyType> DafnyPrint
219        for Tuple1<T0> {
220        fn fmt_print(&self, _formatter: &mut Formatter, _in_seq: bool) -> std::fmt::Result {
221            match self {
222                Tuple1::_T1{_0, } => {
223                    write!(_formatter, "(")?;
224                    DafnyPrint::fmt_print(_0, _formatter, false)?;
225                    write!(_formatter, ")")?;
226                    Ok(())
227                },
228            }
229        }
230    }
231
232    impl<T0: DafnyType> Tuple1<T0> {
233        /// Given type parameter conversions, returns a lambda to convert this structure
234        pub fn coerce<__T0: DafnyType>(f_0: Rc<impl ::std::ops::Fn(T0) -> __T0 + 'static>) -> Rc<impl ::std::ops::Fn(Tuple1<T0>) -> Tuple1<__T0>> {
235            Rc::new(move |this: Self| -> Tuple1<__T0>{
236                    match this {
237                        Tuple1::_T1{_0, } => {
238                            Tuple1::_T1 {
239                                _0: f_0.clone()(_0)
240                            }
241                        },
242                    }
243                })
244        }
245    }
246
247    impl<T0: DafnyType + Eq + Hash> PartialEq
248        for Tuple1<T0> {
249        fn eq(&self, other: &Self) -> bool {
250            match (
251                    self,
252                    other
253                ) {
254                (Tuple1::_T1{_0, }, Tuple1::_T1{_0: _2__0, }) => {
255                    _0 == _2__0
256                },
257                _ => {
258                    false
259                },
260            }
261        }
262    }
263
264    impl<T0: DafnyType + Eq + Hash> Eq
265        for Tuple1<T0> {}
266
267    impl<T0: DafnyType + Hash> Hash
268        for Tuple1<T0> {
269        fn hash<_H: Hasher>(&self, _state: &mut _H) {
270            match self {
271                Tuple1::_T1{_0, } => {
272                    Hash::hash(_0, _state)
273                },
274            }
275        }
276    }
277
278    impl<T0: DafnyType> AsRef<Tuple1<T0>>
279        for Tuple1<T0> {
280        fn as_ref(&self) -> &Self {
281            self
282        }
283    }
284
285    #[derive(Clone)]
286    pub enum Tuple3<T0: DafnyType, T1: DafnyType, T2: DafnyType> {
287        _T3 {
288            _0: T0,
289            _1: T1,
290            _2: T2
291        }
292    }
293
294    impl<T0: DafnyType, T1: DafnyType, T2: DafnyType> Tuple3<T0, T1, T2> {
295        /// Returns a borrow of the field _0
296        pub fn _0(&self) -> &T0 {
297            match self {
298                Tuple3::_T3{_0, _1, _2, } => _0,
299            }
300        }
301        /// Returns a borrow of the field _1
302        pub fn _1(&self) -> &T1 {
303            match self {
304                Tuple3::_T3{_0, _1, _2, } => _1,
305            }
306        }
307        /// Returns a borrow of the field _2
308        pub fn _2(&self) -> &T2 {
309            match self {
310                Tuple3::_T3{_0, _1, _2, } => _2,
311            }
312        }
313    }
314
315    impl<T0: DafnyType, T1: DafnyType, T2: DafnyType> Debug
316        for Tuple3<T0, T1, T2> {
317        fn fmt(&self, f: &mut Formatter) -> Result {
318            DafnyPrint::fmt_print(self, f, true)
319        }
320    }
321
322    impl<T0: DafnyType, T1: DafnyType, T2: DafnyType> DafnyPrint
323        for Tuple3<T0, T1, T2> {
324        fn fmt_print(&self, _formatter: &mut Formatter, _in_seq: bool) -> std::fmt::Result {
325            match self {
326                Tuple3::_T3{_0, _1, _2, } => {
327                    write!(_formatter, "(")?;
328                    DafnyPrint::fmt_print(_0, _formatter, false)?;
329                    write!(_formatter, ", ")?;
330                    DafnyPrint::fmt_print(_1, _formatter, false)?;
331                    write!(_formatter, ", ")?;
332                    DafnyPrint::fmt_print(_2, _formatter, false)?;
333                    write!(_formatter, ")")?;
334                    Ok(())
335                },
336            }
337        }
338    }
339
340    impl<T0: DafnyType, T1: DafnyType, T2: DafnyType> Tuple3<T0, T1, T2> {
341        /// Given type parameter conversions, returns a lambda to convert this structure
342        pub fn coerce<__T0: DafnyType, __T1: DafnyType, __T2: DafnyType>(f_0: Rc<impl ::std::ops::Fn(T0) -> __T0 + 'static>, f_1: Rc<impl ::std::ops::Fn(T1) -> __T1 + 'static>, f_2: Rc<impl ::std::ops::Fn(T2) -> __T2 + 'static>) -> Rc<impl ::std::ops::Fn(Tuple3<T0, T1, T2>) -> Tuple3<__T0, __T1, __T2>> {
343            Rc::new(move |this: Self| -> Tuple3<__T0, __T1, __T2>{
344                    match this {
345                        Tuple3::_T3{_0, _1, _2, } => {
346                            Tuple3::_T3 {
347                                _0: f_0.clone()(_0),
348                                _1: f_1.clone()(_1),
349                                _2: f_2.clone()(_2)
350                            }
351                        },
352                    }
353                })
354        }
355    }
356
357    impl<T0: DafnyType + Eq + Hash, T1: DafnyType + Eq + Hash, T2: DafnyType + Eq + Hash> PartialEq
358        for Tuple3<T0, T1, T2> {
359        fn eq(&self, other: &Self) -> bool {
360            match (
361                    self,
362                    other
363                ) {
364                (Tuple3::_T3{_0, _1, _2, }, Tuple3::_T3{_0: _2__0, _1: _2__1, _2: _2__2, }) => {
365                    _0 == _2__0 && _1 == _2__1 && _2 == _2__2
366                },
367                _ => {
368                    false
369                },
370            }
371        }
372    }
373
374    impl<T0: DafnyType + Eq + Hash, T1: DafnyType + Eq + Hash, T2: DafnyType + Eq + Hash> Eq
375        for Tuple3<T0, T1, T2> {}
376
377    impl<T0: DafnyType + Hash, T1: DafnyType + Hash, T2: DafnyType + Hash> Hash
378        for Tuple3<T0, T1, T2> {
379        fn hash<_H: Hasher>(&self, _state: &mut _H) {
380            match self {
381                Tuple3::_T3{_0, _1, _2, } => {
382                    Hash::hash(_0, _state);
383                    Hash::hash(_1, _state);
384                    Hash::hash(_2, _state)
385                },
386            }
387        }
388    }
389
390    impl<T0: DafnyType, T1: DafnyType, T2: DafnyType> AsRef<Tuple3<T0, T1, T2>>
391        for Tuple3<T0, T1, T2> {
392        fn as_ref(&self) -> &Self {
393            self
394        }
395    }
396
397    #[derive(Clone)]
398    pub enum Tuple4<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType> {
399        _T4 {
400            _0: T0,
401            _1: T1,
402            _2: T2,
403            _3: T3
404        }
405    }
406
407    impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType> Tuple4<T0, T1, T2, T3> {
408        /// Returns a borrow of the field _0
409        pub fn _0(&self) -> &T0 {
410            match self {
411                Tuple4::_T4{_0, _1, _2, _3, } => _0,
412            }
413        }
414        /// Returns a borrow of the field _1
415        pub fn _1(&self) -> &T1 {
416            match self {
417                Tuple4::_T4{_0, _1, _2, _3, } => _1,
418            }
419        }
420        /// Returns a borrow of the field _2
421        pub fn _2(&self) -> &T2 {
422            match self {
423                Tuple4::_T4{_0, _1, _2, _3, } => _2,
424            }
425        }
426        /// Returns a borrow of the field _3
427        pub fn _3(&self) -> &T3 {
428            match self {
429                Tuple4::_T4{_0, _1, _2, _3, } => _3,
430            }
431        }
432    }
433
434    impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType> Debug
435        for Tuple4<T0, T1, T2, T3> {
436        fn fmt(&self, f: &mut Formatter) -> Result {
437            DafnyPrint::fmt_print(self, f, true)
438        }
439    }
440
441    impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType> DafnyPrint
442        for Tuple4<T0, T1, T2, T3> {
443        fn fmt_print(&self, _formatter: &mut Formatter, _in_seq: bool) -> std::fmt::Result {
444            match self {
445                Tuple4::_T4{_0, _1, _2, _3, } => {
446                    write!(_formatter, "(")?;
447                    DafnyPrint::fmt_print(_0, _formatter, false)?;
448                    write!(_formatter, ", ")?;
449                    DafnyPrint::fmt_print(_1, _formatter, false)?;
450                    write!(_formatter, ", ")?;
451                    DafnyPrint::fmt_print(_2, _formatter, false)?;
452                    write!(_formatter, ", ")?;
453                    DafnyPrint::fmt_print(_3, _formatter, false)?;
454                    write!(_formatter, ")")?;
455                    Ok(())
456                },
457            }
458        }
459    }
460
461    impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType> Tuple4<T0, T1, T2, T3> {
462        /// Given type parameter conversions, returns a lambda to convert this structure
463        pub fn coerce<__T0: DafnyType, __T1: DafnyType, __T2: DafnyType, __T3: DafnyType>(f_0: Rc<impl ::std::ops::Fn(T0) -> __T0 + 'static>, f_1: Rc<impl ::std::ops::Fn(T1) -> __T1 + 'static>, f_2: Rc<impl ::std::ops::Fn(T2) -> __T2 + 'static>, f_3: Rc<impl ::std::ops::Fn(T3) -> __T3 + 'static>) -> Rc<impl ::std::ops::Fn(Tuple4<T0, T1, T2, T3>) -> Tuple4<__T0, __T1, __T2, __T3>> {
464            Rc::new(move |this: Self| -> Tuple4<__T0, __T1, __T2, __T3>{
465                    match this {
466                        Tuple4::_T4{_0, _1, _2, _3, } => {
467                            Tuple4::_T4 {
468                                _0: f_0.clone()(_0),
469                                _1: f_1.clone()(_1),
470                                _2: f_2.clone()(_2),
471                                _3: f_3.clone()(_3)
472                            }
473                        },
474                    }
475                })
476        }
477    }
478
479    impl<T0: DafnyType + Eq + Hash, T1: DafnyType + Eq + Hash, T2: DafnyType + Eq + Hash, T3: DafnyType + Eq + Hash> PartialEq
480        for Tuple4<T0, T1, T2, T3> {
481        fn eq(&self, other: &Self) -> bool {
482            match (
483                    self,
484                    other
485                ) {
486                (Tuple4::_T4{_0, _1, _2, _3, }, Tuple4::_T4{_0: _2__0, _1: _2__1, _2: _2__2, _3: _2__3, }) => {
487                    _0 == _2__0 && _1 == _2__1 && _2 == _2__2 && _3 == _2__3
488                },
489                _ => {
490                    false
491                },
492            }
493        }
494    }
495
496    impl<T0: DafnyType + Eq + Hash, T1: DafnyType + Eq + Hash, T2: DafnyType + Eq + Hash, T3: DafnyType + Eq + Hash> Eq
497        for Tuple4<T0, T1, T2, T3> {}
498
499    impl<T0: DafnyType + Hash, T1: DafnyType + Hash, T2: DafnyType + Hash, T3: DafnyType + Hash> Hash
500        for Tuple4<T0, T1, T2, T3> {
501        fn hash<_H: Hasher>(&self, _state: &mut _H) {
502            match self {
503                Tuple4::_T4{_0, _1, _2, _3, } => {
504                    Hash::hash(_0, _state);
505                    Hash::hash(_1, _state);
506                    Hash::hash(_2, _state);
507                    Hash::hash(_3, _state)
508                },
509            }
510        }
511    }
512
513    impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType> AsRef<Tuple4<T0, T1, T2, T3>>
514        for Tuple4<T0, T1, T2, T3> {
515        fn as_ref(&self) -> &Self {
516            self
517        }
518    }
519
520    #[derive(Clone)]
521    pub enum Tuple5<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType> {
522        _T5 {
523            _0: T0,
524            _1: T1,
525            _2: T2,
526            _3: T3,
527            _4: T4
528        }
529    }
530
531    impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType> Tuple5<T0, T1, T2, T3, T4> {
532        /// Returns a borrow of the field _0
533        pub fn _0(&self) -> &T0 {
534            match self {
535                Tuple5::_T5{_0, _1, _2, _3, _4, } => _0,
536            }
537        }
538        /// Returns a borrow of the field _1
539        pub fn _1(&self) -> &T1 {
540            match self {
541                Tuple5::_T5{_0, _1, _2, _3, _4, } => _1,
542            }
543        }
544        /// Returns a borrow of the field _2
545        pub fn _2(&self) -> &T2 {
546            match self {
547                Tuple5::_T5{_0, _1, _2, _3, _4, } => _2,
548            }
549        }
550        /// Returns a borrow of the field _3
551        pub fn _3(&self) -> &T3 {
552            match self {
553                Tuple5::_T5{_0, _1, _2, _3, _4, } => _3,
554            }
555        }
556        /// Returns a borrow of the field _4
557        pub fn _4(&self) -> &T4 {
558            match self {
559                Tuple5::_T5{_0, _1, _2, _3, _4, } => _4,
560            }
561        }
562    }
563
564    impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType> Debug
565        for Tuple5<T0, T1, T2, T3, T4> {
566        fn fmt(&self, f: &mut Formatter) -> Result {
567            DafnyPrint::fmt_print(self, f, true)
568        }
569    }
570
571    impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType> DafnyPrint
572        for Tuple5<T0, T1, T2, T3, T4> {
573        fn fmt_print(&self, _formatter: &mut Formatter, _in_seq: bool) -> std::fmt::Result {
574            match self {
575                Tuple5::_T5{_0, _1, _2, _3, _4, } => {
576                    write!(_formatter, "(")?;
577                    DafnyPrint::fmt_print(_0, _formatter, false)?;
578                    write!(_formatter, ", ")?;
579                    DafnyPrint::fmt_print(_1, _formatter, false)?;
580                    write!(_formatter, ", ")?;
581                    DafnyPrint::fmt_print(_2, _formatter, false)?;
582                    write!(_formatter, ", ")?;
583                    DafnyPrint::fmt_print(_3, _formatter, false)?;
584                    write!(_formatter, ", ")?;
585                    DafnyPrint::fmt_print(_4, _formatter, false)?;
586                    write!(_formatter, ")")?;
587                    Ok(())
588                },
589            }
590        }
591    }
592
593    impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType> Tuple5<T0, T1, T2, T3, T4> {
594        /// Given type parameter conversions, returns a lambda to convert this structure
595        pub fn coerce<__T0: DafnyType, __T1: DafnyType, __T2: DafnyType, __T3: DafnyType, __T4: DafnyType>(f_0: Rc<impl ::std::ops::Fn(T0) -> __T0 + 'static>, f_1: Rc<impl ::std::ops::Fn(T1) -> __T1 + 'static>, f_2: Rc<impl ::std::ops::Fn(T2) -> __T2 + 'static>, f_3: Rc<impl ::std::ops::Fn(T3) -> __T3 + 'static>, f_4: Rc<impl ::std::ops::Fn(T4) -> __T4 + 'static>) -> Rc<impl ::std::ops::Fn(Tuple5<T0, T1, T2, T3, T4>) -> Tuple5<__T0, __T1, __T2, __T3, __T4>> {
596            Rc::new(move |this: Self| -> Tuple5<__T0, __T1, __T2, __T3, __T4>{
597                    match this {
598                        Tuple5::_T5{_0, _1, _2, _3, _4, } => {
599                            Tuple5::_T5 {
600                                _0: f_0.clone()(_0),
601                                _1: f_1.clone()(_1),
602                                _2: f_2.clone()(_2),
603                                _3: f_3.clone()(_3),
604                                _4: f_4.clone()(_4)
605                            }
606                        },
607                    }
608                })
609        }
610    }
611
612    impl<T0: DafnyType + Eq + Hash, T1: DafnyType + Eq + Hash, T2: DafnyType + Eq + Hash, T3: DafnyType + Eq + Hash, T4: DafnyType + Eq + Hash> PartialEq
613        for Tuple5<T0, T1, T2, T3, T4> {
614        fn eq(&self, other: &Self) -> bool {
615            match (
616                    self,
617                    other
618                ) {
619                (Tuple5::_T5{_0, _1, _2, _3, _4, }, Tuple5::_T5{_0: _2__0, _1: _2__1, _2: _2__2, _3: _2__3, _4: _2__4, }) => {
620                    _0 == _2__0 && _1 == _2__1 && _2 == _2__2 && _3 == _2__3 && _4 == _2__4
621                },
622                _ => {
623                    false
624                },
625            }
626        }
627    }
628
629    impl<T0: DafnyType + Eq + Hash, T1: DafnyType + Eq + Hash, T2: DafnyType + Eq + Hash, T3: DafnyType + Eq + Hash, T4: DafnyType + Eq + Hash> Eq
630        for Tuple5<T0, T1, T2, T3, T4> {}
631
632    impl<T0: DafnyType + Hash, T1: DafnyType + Hash, T2: DafnyType + Hash, T3: DafnyType + Hash, T4: DafnyType + Hash> Hash
633        for Tuple5<T0, T1, T2, T3, T4> {
634        fn hash<_H: Hasher>(&self, _state: &mut _H) {
635            match self {
636                Tuple5::_T5{_0, _1, _2, _3, _4, } => {
637                    Hash::hash(_0, _state);
638                    Hash::hash(_1, _state);
639                    Hash::hash(_2, _state);
640                    Hash::hash(_3, _state);
641                    Hash::hash(_4, _state)
642                },
643            }
644        }
645    }
646
647    impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType> AsRef<Tuple5<T0, T1, T2, T3, T4>>
648        for Tuple5<T0, T1, T2, T3, T4> {
649        fn as_ref(&self) -> &Self {
650            self
651        }
652    }
653
654    #[derive(Clone)]
655    pub enum Tuple6<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType> {
656        _T6 {
657            _0: T0,
658            _1: T1,
659            _2: T2,
660            _3: T3,
661            _4: T4,
662            _5: T5
663        }
664    }
665
666    impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType> Tuple6<T0, T1, T2, T3, T4, T5> {
667        /// Returns a borrow of the field _0
668        pub fn _0(&self) -> &T0 {
669            match self {
670                Tuple6::_T6{_0, _1, _2, _3, _4, _5, } => _0,
671            }
672        }
673        /// Returns a borrow of the field _1
674        pub fn _1(&self) -> &T1 {
675            match self {
676                Tuple6::_T6{_0, _1, _2, _3, _4, _5, } => _1,
677            }
678        }
679        /// Returns a borrow of the field _2
680        pub fn _2(&self) -> &T2 {
681            match self {
682                Tuple6::_T6{_0, _1, _2, _3, _4, _5, } => _2,
683            }
684        }
685        /// Returns a borrow of the field _3
686        pub fn _3(&self) -> &T3 {
687            match self {
688                Tuple6::_T6{_0, _1, _2, _3, _4, _5, } => _3,
689            }
690        }
691        /// Returns a borrow of the field _4
692        pub fn _4(&self) -> &T4 {
693            match self {
694                Tuple6::_T6{_0, _1, _2, _3, _4, _5, } => _4,
695            }
696        }
697        /// Returns a borrow of the field _5
698        pub fn _5(&self) -> &T5 {
699            match self {
700                Tuple6::_T6{_0, _1, _2, _3, _4, _5, } => _5,
701            }
702        }
703    }
704
705    impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType> Debug
706        for Tuple6<T0, T1, T2, T3, T4, T5> {
707        fn fmt(&self, f: &mut Formatter) -> Result {
708            DafnyPrint::fmt_print(self, f, true)
709        }
710    }
711
712    impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType> DafnyPrint
713        for Tuple6<T0, T1, T2, T3, T4, T5> {
714        fn fmt_print(&self, _formatter: &mut Formatter, _in_seq: bool) -> std::fmt::Result {
715            match self {
716                Tuple6::_T6{_0, _1, _2, _3, _4, _5, } => {
717                    write!(_formatter, "(")?;
718                    DafnyPrint::fmt_print(_0, _formatter, false)?;
719                    write!(_formatter, ", ")?;
720                    DafnyPrint::fmt_print(_1, _formatter, false)?;
721                    write!(_formatter, ", ")?;
722                    DafnyPrint::fmt_print(_2, _formatter, false)?;
723                    write!(_formatter, ", ")?;
724                    DafnyPrint::fmt_print(_3, _formatter, false)?;
725                    write!(_formatter, ", ")?;
726                    DafnyPrint::fmt_print(_4, _formatter, false)?;
727                    write!(_formatter, ", ")?;
728                    DafnyPrint::fmt_print(_5, _formatter, false)?;
729                    write!(_formatter, ")")?;
730                    Ok(())
731                },
732            }
733        }
734    }
735
736    impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType> Tuple6<T0, T1, T2, T3, T4, T5> {
737        /// Given type parameter conversions, returns a lambda to convert this structure
738        pub fn coerce<__T0: DafnyType, __T1: DafnyType, __T2: DafnyType, __T3: DafnyType, __T4: DafnyType, __T5: DafnyType>(f_0: Rc<impl ::std::ops::Fn(T0) -> __T0 + 'static>, f_1: Rc<impl ::std::ops::Fn(T1) -> __T1 + 'static>, f_2: Rc<impl ::std::ops::Fn(T2) -> __T2 + 'static>, f_3: Rc<impl ::std::ops::Fn(T3) -> __T3 + 'static>, f_4: Rc<impl ::std::ops::Fn(T4) -> __T4 + 'static>, f_5: Rc<impl ::std::ops::Fn(T5) -> __T5 + 'static>) -> Rc<impl ::std::ops::Fn(Tuple6<T0, T1, T2, T3, T4, T5>) -> Tuple6<__T0, __T1, __T2, __T3, __T4, __T5>> {
739            Rc::new(move |this: Self| -> Tuple6<__T0, __T1, __T2, __T3, __T4, __T5>{
740                    match this {
741                        Tuple6::_T6{_0, _1, _2, _3, _4, _5, } => {
742                            Tuple6::_T6 {
743                                _0: f_0.clone()(_0),
744                                _1: f_1.clone()(_1),
745                                _2: f_2.clone()(_2),
746                                _3: f_3.clone()(_3),
747                                _4: f_4.clone()(_4),
748                                _5: f_5.clone()(_5)
749                            }
750                        },
751                    }
752                })
753        }
754    }
755
756    impl<T0: DafnyType + Eq + Hash, T1: DafnyType + Eq + Hash, T2: DafnyType + Eq + Hash, T3: DafnyType + Eq + Hash, T4: DafnyType + Eq + Hash, T5: DafnyType + Eq + Hash> PartialEq
757        for Tuple6<T0, T1, T2, T3, T4, T5> {
758        fn eq(&self, other: &Self) -> bool {
759            match (
760                    self,
761                    other
762                ) {
763                (Tuple6::_T6{_0, _1, _2, _3, _4, _5, }, Tuple6::_T6{_0: _2__0, _1: _2__1, _2: _2__2, _3: _2__3, _4: _2__4, _5: _2__5, }) => {
764                    _0 == _2__0 && _1 == _2__1 && _2 == _2__2 && _3 == _2__3 && _4 == _2__4 && _5 == _2__5
765                },
766                _ => {
767                    false
768                },
769            }
770        }
771    }
772
773    impl<T0: DafnyType + Eq + Hash, T1: DafnyType + Eq + Hash, T2: DafnyType + Eq + Hash, T3: DafnyType + Eq + Hash, T4: DafnyType + Eq + Hash, T5: DafnyType + Eq + Hash> Eq
774        for Tuple6<T0, T1, T2, T3, T4, T5> {}
775
776    impl<T0: DafnyType + Hash, T1: DafnyType + Hash, T2: DafnyType + Hash, T3: DafnyType + Hash, T4: DafnyType + Hash, T5: DafnyType + Hash> Hash
777        for Tuple6<T0, T1, T2, T3, T4, T5> {
778        fn hash<_H: Hasher>(&self, _state: &mut _H) {
779            match self {
780                Tuple6::_T6{_0, _1, _2, _3, _4, _5, } => {
781                    Hash::hash(_0, _state);
782                    Hash::hash(_1, _state);
783                    Hash::hash(_2, _state);
784                    Hash::hash(_3, _state);
785                    Hash::hash(_4, _state);
786                    Hash::hash(_5, _state)
787                },
788            }
789        }
790    }
791
792    impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType> AsRef<Tuple6<T0, T1, T2, T3, T4, T5>>
793        for Tuple6<T0, T1, T2, T3, T4, T5> {
794        fn as_ref(&self) -> &Self {
795            self
796        }
797    }
798
799    #[derive(Clone)]
800    pub enum Tuple7<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType> {
801        _T7 {
802            _0: T0,
803            _1: T1,
804            _2: T2,
805            _3: T3,
806            _4: T4,
807            _5: T5,
808            _6: T6
809        }
810    }
811
812    impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType> Tuple7<T0, T1, T2, T3, T4, T5, T6> {
813        /// Returns a borrow of the field _0
814        pub fn _0(&self) -> &T0 {
815            match self {
816                Tuple7::_T7{_0, _1, _2, _3, _4, _5, _6, } => _0,
817            }
818        }
819        /// Returns a borrow of the field _1
820        pub fn _1(&self) -> &T1 {
821            match self {
822                Tuple7::_T7{_0, _1, _2, _3, _4, _5, _6, } => _1,
823            }
824        }
825        /// Returns a borrow of the field _2
826        pub fn _2(&self) -> &T2 {
827            match self {
828                Tuple7::_T7{_0, _1, _2, _3, _4, _5, _6, } => _2,
829            }
830        }
831        /// Returns a borrow of the field _3
832        pub fn _3(&self) -> &T3 {
833            match self {
834                Tuple7::_T7{_0, _1, _2, _3, _4, _5, _6, } => _3,
835            }
836        }
837        /// Returns a borrow of the field _4
838        pub fn _4(&self) -> &T4 {
839            match self {
840                Tuple7::_T7{_0, _1, _2, _3, _4, _5, _6, } => _4,
841            }
842        }
843        /// Returns a borrow of the field _5
844        pub fn _5(&self) -> &T5 {
845            match self {
846                Tuple7::_T7{_0, _1, _2, _3, _4, _5, _6, } => _5,
847            }
848        }
849        /// Returns a borrow of the field _6
850        pub fn _6(&self) -> &T6 {
851            match self {
852                Tuple7::_T7{_0, _1, _2, _3, _4, _5, _6, } => _6,
853            }
854        }
855    }
856
857    impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType> Debug
858        for Tuple7<T0, T1, T2, T3, T4, T5, T6> {
859        fn fmt(&self, f: &mut Formatter) -> Result {
860            DafnyPrint::fmt_print(self, f, true)
861        }
862    }
863
864    impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType> DafnyPrint
865        for Tuple7<T0, T1, T2, T3, T4, T5, T6> {
866        fn fmt_print(&self, _formatter: &mut Formatter, _in_seq: bool) -> std::fmt::Result {
867            match self {
868                Tuple7::_T7{_0, _1, _2, _3, _4, _5, _6, } => {
869                    write!(_formatter, "(")?;
870                    DafnyPrint::fmt_print(_0, _formatter, false)?;
871                    write!(_formatter, ", ")?;
872                    DafnyPrint::fmt_print(_1, _formatter, false)?;
873                    write!(_formatter, ", ")?;
874                    DafnyPrint::fmt_print(_2, _formatter, false)?;
875                    write!(_formatter, ", ")?;
876                    DafnyPrint::fmt_print(_3, _formatter, false)?;
877                    write!(_formatter, ", ")?;
878                    DafnyPrint::fmt_print(_4, _formatter, false)?;
879                    write!(_formatter, ", ")?;
880                    DafnyPrint::fmt_print(_5, _formatter, false)?;
881                    write!(_formatter, ", ")?;
882                    DafnyPrint::fmt_print(_6, _formatter, false)?;
883                    write!(_formatter, ")")?;
884                    Ok(())
885                },
886            }
887        }
888    }
889
890    impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType> Tuple7<T0, T1, T2, T3, T4, T5, T6> {
891        /// Given type parameter conversions, returns a lambda to convert this structure
892        pub fn coerce<__T0: DafnyType, __T1: DafnyType, __T2: DafnyType, __T3: DafnyType, __T4: DafnyType, __T5: DafnyType, __T6: DafnyType>(f_0: Rc<impl ::std::ops::Fn(T0) -> __T0 + 'static>, f_1: Rc<impl ::std::ops::Fn(T1) -> __T1 + 'static>, f_2: Rc<impl ::std::ops::Fn(T2) -> __T2 + 'static>, f_3: Rc<impl ::std::ops::Fn(T3) -> __T3 + 'static>, f_4: Rc<impl ::std::ops::Fn(T4) -> __T4 + 'static>, f_5: Rc<impl ::std::ops::Fn(T5) -> __T5 + 'static>, f_6: Rc<impl ::std::ops::Fn(T6) -> __T6 + 'static>) -> Rc<impl ::std::ops::Fn(Tuple7<T0, T1, T2, T3, T4, T5, T6>) -> Tuple7<__T0, __T1, __T2, __T3, __T4, __T5, __T6>> {
893            Rc::new(move |this: Self| -> Tuple7<__T0, __T1, __T2, __T3, __T4, __T5, __T6>{
894                    match this {
895                        Tuple7::_T7{_0, _1, _2, _3, _4, _5, _6, } => {
896                            Tuple7::_T7 {
897                                _0: f_0.clone()(_0),
898                                _1: f_1.clone()(_1),
899                                _2: f_2.clone()(_2),
900                                _3: f_3.clone()(_3),
901                                _4: f_4.clone()(_4),
902                                _5: f_5.clone()(_5),
903                                _6: f_6.clone()(_6)
904                            }
905                        },
906                    }
907                })
908        }
909    }
910
911    impl<T0: DafnyType + Eq + Hash, T1: DafnyType + Eq + Hash, T2: DafnyType + Eq + Hash, T3: DafnyType + Eq + Hash, T4: DafnyType + Eq + Hash, T5: DafnyType + Eq + Hash, T6: DafnyType + Eq + Hash> PartialEq
912        for Tuple7<T0, T1, T2, T3, T4, T5, T6> {
913        fn eq(&self, other: &Self) -> bool {
914            match (
915                    self,
916                    other
917                ) {
918                (Tuple7::_T7{_0, _1, _2, _3, _4, _5, _6, }, Tuple7::_T7{_0: _2__0, _1: _2__1, _2: _2__2, _3: _2__3, _4: _2__4, _5: _2__5, _6: _2__6, }) => {
919                    _0 == _2__0 && _1 == _2__1 && _2 == _2__2 && _3 == _2__3 && _4 == _2__4 && _5 == _2__5 && _6 == _2__6
920                },
921                _ => {
922                    false
923                },
924            }
925        }
926    }
927
928    impl<T0: DafnyType + Eq + Hash, T1: DafnyType + Eq + Hash, T2: DafnyType + Eq + Hash, T3: DafnyType + Eq + Hash, T4: DafnyType + Eq + Hash, T5: DafnyType + Eq + Hash, T6: DafnyType + Eq + Hash> Eq
929        for Tuple7<T0, T1, T2, T3, T4, T5, T6> {}
930
931    impl<T0: DafnyType + Hash, T1: DafnyType + Hash, T2: DafnyType + Hash, T3: DafnyType + Hash, T4: DafnyType + Hash, T5: DafnyType + Hash, T6: DafnyType + Hash> Hash
932        for Tuple7<T0, T1, T2, T3, T4, T5, T6> {
933        fn hash<_H: Hasher>(&self, _state: &mut _H) {
934            match self {
935                Tuple7::_T7{_0, _1, _2, _3, _4, _5, _6, } => {
936                    Hash::hash(_0, _state);
937                    Hash::hash(_1, _state);
938                    Hash::hash(_2, _state);
939                    Hash::hash(_3, _state);
940                    Hash::hash(_4, _state);
941                    Hash::hash(_5, _state);
942                    Hash::hash(_6, _state)
943                },
944            }
945        }
946    }
947
948    impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType> AsRef<Tuple7<T0, T1, T2, T3, T4, T5, T6>>
949        for Tuple7<T0, T1, T2, T3, T4, T5, T6> {
950        fn as_ref(&self) -> &Self {
951            self
952        }
953    }
954
955    #[derive(Clone)]
956    pub enum Tuple8<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType> {
957        _T8 {
958            _0: T0,
959            _1: T1,
960            _2: T2,
961            _3: T3,
962            _4: T4,
963            _5: T5,
964            _6: T6,
965            _7: T7
966        }
967    }
968
969    impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType> Tuple8<T0, T1, T2, T3, T4, T5, T6, T7> {
970        /// Returns a borrow of the field _0
971        pub fn _0(&self) -> &T0 {
972            match self {
973                Tuple8::_T8{_0, _1, _2, _3, _4, _5, _6, _7, } => _0,
974            }
975        }
976        /// Returns a borrow of the field _1
977        pub fn _1(&self) -> &T1 {
978            match self {
979                Tuple8::_T8{_0, _1, _2, _3, _4, _5, _6, _7, } => _1,
980            }
981        }
982        /// Returns a borrow of the field _2
983        pub fn _2(&self) -> &T2 {
984            match self {
985                Tuple8::_T8{_0, _1, _2, _3, _4, _5, _6, _7, } => _2,
986            }
987        }
988        /// Returns a borrow of the field _3
989        pub fn _3(&self) -> &T3 {
990            match self {
991                Tuple8::_T8{_0, _1, _2, _3, _4, _5, _6, _7, } => _3,
992            }
993        }
994        /// Returns a borrow of the field _4
995        pub fn _4(&self) -> &T4 {
996            match self {
997                Tuple8::_T8{_0, _1, _2, _3, _4, _5, _6, _7, } => _4,
998            }
999        }
1000        /// Returns a borrow of the field _5
1001        pub fn _5(&self) -> &T5 {
1002            match self {
1003                Tuple8::_T8{_0, _1, _2, _3, _4, _5, _6, _7, } => _5,
1004            }
1005        }
1006        /// Returns a borrow of the field _6
1007        pub fn _6(&self) -> &T6 {
1008            match self {
1009                Tuple8::_T8{_0, _1, _2, _3, _4, _5, _6, _7, } => _6,
1010            }
1011        }
1012        /// Returns a borrow of the field _7
1013        pub fn _7(&self) -> &T7 {
1014            match self {
1015                Tuple8::_T8{_0, _1, _2, _3, _4, _5, _6, _7, } => _7,
1016            }
1017        }
1018    }
1019
1020    impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType> Debug
1021        for Tuple8<T0, T1, T2, T3, T4, T5, T6, T7> {
1022        fn fmt(&self, f: &mut Formatter) -> Result {
1023            DafnyPrint::fmt_print(self, f, true)
1024        }
1025    }
1026
1027    impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType> DafnyPrint
1028        for Tuple8<T0, T1, T2, T3, T4, T5, T6, T7> {
1029        fn fmt_print(&self, _formatter: &mut Formatter, _in_seq: bool) -> std::fmt::Result {
1030            match self {
1031                Tuple8::_T8{_0, _1, _2, _3, _4, _5, _6, _7, } => {
1032                    write!(_formatter, "(")?;
1033                    DafnyPrint::fmt_print(_0, _formatter, false)?;
1034                    write!(_formatter, ", ")?;
1035                    DafnyPrint::fmt_print(_1, _formatter, false)?;
1036                    write!(_formatter, ", ")?;
1037                    DafnyPrint::fmt_print(_2, _formatter, false)?;
1038                    write!(_formatter, ", ")?;
1039                    DafnyPrint::fmt_print(_3, _formatter, false)?;
1040                    write!(_formatter, ", ")?;
1041                    DafnyPrint::fmt_print(_4, _formatter, false)?;
1042                    write!(_formatter, ", ")?;
1043                    DafnyPrint::fmt_print(_5, _formatter, false)?;
1044                    write!(_formatter, ", ")?;
1045                    DafnyPrint::fmt_print(_6, _formatter, false)?;
1046                    write!(_formatter, ", ")?;
1047                    DafnyPrint::fmt_print(_7, _formatter, false)?;
1048                    write!(_formatter, ")")?;
1049                    Ok(())
1050                },
1051            }
1052        }
1053    }
1054
1055    impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType> Tuple8<T0, T1, T2, T3, T4, T5, T6, T7> {
1056        /// Given type parameter conversions, returns a lambda to convert this structure
1057        pub fn coerce<__T0: DafnyType, __T1: DafnyType, __T2: DafnyType, __T3: DafnyType, __T4: DafnyType, __T5: DafnyType, __T6: DafnyType, __T7: DafnyType>(f_0: Rc<impl ::std::ops::Fn(T0) -> __T0 + 'static>, f_1: Rc<impl ::std::ops::Fn(T1) -> __T1 + 'static>, f_2: Rc<impl ::std::ops::Fn(T2) -> __T2 + 'static>, f_3: Rc<impl ::std::ops::Fn(T3) -> __T3 + 'static>, f_4: Rc<impl ::std::ops::Fn(T4) -> __T4 + 'static>, f_5: Rc<impl ::std::ops::Fn(T5) -> __T5 + 'static>, f_6: Rc<impl ::std::ops::Fn(T6) -> __T6 + 'static>, f_7: Rc<impl ::std::ops::Fn(T7) -> __T7 + 'static>) -> Rc<impl ::std::ops::Fn(Tuple8<T0, T1, T2, T3, T4, T5, T6, T7>) -> Tuple8<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7>> {
1058            Rc::new(move |this: Self| -> Tuple8<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7>{
1059                    match this {
1060                        Tuple8::_T8{_0, _1, _2, _3, _4, _5, _6, _7, } => {
1061                            Tuple8::_T8 {
1062                                _0: f_0.clone()(_0),
1063                                _1: f_1.clone()(_1),
1064                                _2: f_2.clone()(_2),
1065                                _3: f_3.clone()(_3),
1066                                _4: f_4.clone()(_4),
1067                                _5: f_5.clone()(_5),
1068                                _6: f_6.clone()(_6),
1069                                _7: f_7.clone()(_7)
1070                            }
1071                        },
1072                    }
1073                })
1074        }
1075    }
1076
1077    impl<T0: DafnyType + Eq + Hash, T1: DafnyType + Eq + Hash, T2: DafnyType + Eq + Hash, T3: DafnyType + Eq + Hash, T4: DafnyType + Eq + Hash, T5: DafnyType + Eq + Hash, T6: DafnyType + Eq + Hash, T7: DafnyType + Eq + Hash> PartialEq
1078        for Tuple8<T0, T1, T2, T3, T4, T5, T6, T7> {
1079        fn eq(&self, other: &Self) -> bool {
1080            match (
1081                    self,
1082                    other
1083                ) {
1084                (Tuple8::_T8{_0, _1, _2, _3, _4, _5, _6, _7, }, Tuple8::_T8{_0: _2__0, _1: _2__1, _2: _2__2, _3: _2__3, _4: _2__4, _5: _2__5, _6: _2__6, _7: _2__7, }) => {
1085                    _0 == _2__0 && _1 == _2__1 && _2 == _2__2 && _3 == _2__3 && _4 == _2__4 && _5 == _2__5 && _6 == _2__6 && _7 == _2__7
1086                },
1087                _ => {
1088                    false
1089                },
1090            }
1091        }
1092    }
1093
1094    impl<T0: DafnyType + Eq + Hash, T1: DafnyType + Eq + Hash, T2: DafnyType + Eq + Hash, T3: DafnyType + Eq + Hash, T4: DafnyType + Eq + Hash, T5: DafnyType + Eq + Hash, T6: DafnyType + Eq + Hash, T7: DafnyType + Eq + Hash> Eq
1095        for Tuple8<T0, T1, T2, T3, T4, T5, T6, T7> {}
1096
1097    impl<T0: DafnyType + Hash, T1: DafnyType + Hash, T2: DafnyType + Hash, T3: DafnyType + Hash, T4: DafnyType + Hash, T5: DafnyType + Hash, T6: DafnyType + Hash, T7: DafnyType + Hash> Hash
1098        for Tuple8<T0, T1, T2, T3, T4, T5, T6, T7> {
1099        fn hash<_H: Hasher>(&self, _state: &mut _H) {
1100            match self {
1101                Tuple8::_T8{_0, _1, _2, _3, _4, _5, _6, _7, } => {
1102                    Hash::hash(_0, _state);
1103                    Hash::hash(_1, _state);
1104                    Hash::hash(_2, _state);
1105                    Hash::hash(_3, _state);
1106                    Hash::hash(_4, _state);
1107                    Hash::hash(_5, _state);
1108                    Hash::hash(_6, _state);
1109                    Hash::hash(_7, _state)
1110                },
1111            }
1112        }
1113    }
1114
1115    impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType> AsRef<Tuple8<T0, T1, T2, T3, T4, T5, T6, T7>>
1116        for Tuple8<T0, T1, T2, T3, T4, T5, T6, T7> {
1117        fn as_ref(&self) -> &Self {
1118            self
1119        }
1120    }
1121
1122    #[derive(Clone)]
1123    pub enum Tuple9<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType> {
1124        _T9 {
1125            _0: T0,
1126            _1: T1,
1127            _2: T2,
1128            _3: T3,
1129            _4: T4,
1130            _5: T5,
1131            _6: T6,
1132            _7: T7,
1133            _8: T8
1134        }
1135    }
1136
1137    impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType> Tuple9<T0, T1, T2, T3, T4, T5, T6, T7, T8> {
1138        /// Returns a borrow of the field _0
1139        pub fn _0(&self) -> &T0 {
1140            match self {
1141                Tuple9::_T9{_0, _1, _2, _3, _4, _5, _6, _7, _8, } => _0,
1142            }
1143        }
1144        /// Returns a borrow of the field _1
1145        pub fn _1(&self) -> &T1 {
1146            match self {
1147                Tuple9::_T9{_0, _1, _2, _3, _4, _5, _6, _7, _8, } => _1,
1148            }
1149        }
1150        /// Returns a borrow of the field _2
1151        pub fn _2(&self) -> &T2 {
1152            match self {
1153                Tuple9::_T9{_0, _1, _2, _3, _4, _5, _6, _7, _8, } => _2,
1154            }
1155        }
1156        /// Returns a borrow of the field _3
1157        pub fn _3(&self) -> &T3 {
1158            match self {
1159                Tuple9::_T9{_0, _1, _2, _3, _4, _5, _6, _7, _8, } => _3,
1160            }
1161        }
1162        /// Returns a borrow of the field _4
1163        pub fn _4(&self) -> &T4 {
1164            match self {
1165                Tuple9::_T9{_0, _1, _2, _3, _4, _5, _6, _7, _8, } => _4,
1166            }
1167        }
1168        /// Returns a borrow of the field _5
1169        pub fn _5(&self) -> &T5 {
1170            match self {
1171                Tuple9::_T9{_0, _1, _2, _3, _4, _5, _6, _7, _8, } => _5,
1172            }
1173        }
1174        /// Returns a borrow of the field _6
1175        pub fn _6(&self) -> &T6 {
1176            match self {
1177                Tuple9::_T9{_0, _1, _2, _3, _4, _5, _6, _7, _8, } => _6,
1178            }
1179        }
1180        /// Returns a borrow of the field _7
1181        pub fn _7(&self) -> &T7 {
1182            match self {
1183                Tuple9::_T9{_0, _1, _2, _3, _4, _5, _6, _7, _8, } => _7,
1184            }
1185        }
1186        /// Returns a borrow of the field _8
1187        pub fn _8(&self) -> &T8 {
1188            match self {
1189                Tuple9::_T9{_0, _1, _2, _3, _4, _5, _6, _7, _8, } => _8,
1190            }
1191        }
1192    }
1193
1194    impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType> Debug
1195        for Tuple9<T0, T1, T2, T3, T4, T5, T6, T7, T8> {
1196        fn fmt(&self, f: &mut Formatter) -> Result {
1197            DafnyPrint::fmt_print(self, f, true)
1198        }
1199    }
1200
1201    impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType> DafnyPrint
1202        for Tuple9<T0, T1, T2, T3, T4, T5, T6, T7, T8> {
1203        fn fmt_print(&self, _formatter: &mut Formatter, _in_seq: bool) -> std::fmt::Result {
1204            match self {
1205                Tuple9::_T9{_0, _1, _2, _3, _4, _5, _6, _7, _8, } => {
1206                    write!(_formatter, "(")?;
1207                    DafnyPrint::fmt_print(_0, _formatter, false)?;
1208                    write!(_formatter, ", ")?;
1209                    DafnyPrint::fmt_print(_1, _formatter, false)?;
1210                    write!(_formatter, ", ")?;
1211                    DafnyPrint::fmt_print(_2, _formatter, false)?;
1212                    write!(_formatter, ", ")?;
1213                    DafnyPrint::fmt_print(_3, _formatter, false)?;
1214                    write!(_formatter, ", ")?;
1215                    DafnyPrint::fmt_print(_4, _formatter, false)?;
1216                    write!(_formatter, ", ")?;
1217                    DafnyPrint::fmt_print(_5, _formatter, false)?;
1218                    write!(_formatter, ", ")?;
1219                    DafnyPrint::fmt_print(_6, _formatter, false)?;
1220                    write!(_formatter, ", ")?;
1221                    DafnyPrint::fmt_print(_7, _formatter, false)?;
1222                    write!(_formatter, ", ")?;
1223                    DafnyPrint::fmt_print(_8, _formatter, false)?;
1224                    write!(_formatter, ")")?;
1225                    Ok(())
1226                },
1227            }
1228        }
1229    }
1230
1231    impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType> Tuple9<T0, T1, T2, T3, T4, T5, T6, T7, T8> {
1232        /// Given type parameter conversions, returns a lambda to convert this structure
1233        pub fn coerce<__T0: DafnyType, __T1: DafnyType, __T2: DafnyType, __T3: DafnyType, __T4: DafnyType, __T5: DafnyType, __T6: DafnyType, __T7: DafnyType, __T8: DafnyType>(f_0: Rc<impl ::std::ops::Fn(T0) -> __T0 + 'static>, f_1: Rc<impl ::std::ops::Fn(T1) -> __T1 + 'static>, f_2: Rc<impl ::std::ops::Fn(T2) -> __T2 + 'static>, f_3: Rc<impl ::std::ops::Fn(T3) -> __T3 + 'static>, f_4: Rc<impl ::std::ops::Fn(T4) -> __T4 + 'static>, f_5: Rc<impl ::std::ops::Fn(T5) -> __T5 + 'static>, f_6: Rc<impl ::std::ops::Fn(T6) -> __T6 + 'static>, f_7: Rc<impl ::std::ops::Fn(T7) -> __T7 + 'static>, f_8: Rc<impl ::std::ops::Fn(T8) -> __T8 + 'static>) -> Rc<impl ::std::ops::Fn(Tuple9<T0, T1, T2, T3, T4, T5, T6, T7, T8>) -> Tuple9<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8>> {
1234            Rc::new(move |this: Self| -> Tuple9<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8>{
1235                    match this {
1236                        Tuple9::_T9{_0, _1, _2, _3, _4, _5, _6, _7, _8, } => {
1237                            Tuple9::_T9 {
1238                                _0: f_0.clone()(_0),
1239                                _1: f_1.clone()(_1),
1240                                _2: f_2.clone()(_2),
1241                                _3: f_3.clone()(_3),
1242                                _4: f_4.clone()(_4),
1243                                _5: f_5.clone()(_5),
1244                                _6: f_6.clone()(_6),
1245                                _7: f_7.clone()(_7),
1246                                _8: f_8.clone()(_8)
1247                            }
1248                        },
1249                    }
1250                })
1251        }
1252    }
1253
1254    impl<T0: DafnyType + Eq + Hash, T1: DafnyType + Eq + Hash, T2: DafnyType + Eq + Hash, T3: DafnyType + Eq + Hash, T4: DafnyType + Eq + Hash, T5: DafnyType + Eq + Hash, T6: DafnyType + Eq + Hash, T7: DafnyType + Eq + Hash, T8: DafnyType + Eq + Hash> PartialEq
1255        for Tuple9<T0, T1, T2, T3, T4, T5, T6, T7, T8> {
1256        fn eq(&self, other: &Self) -> bool {
1257            match (
1258                    self,
1259                    other
1260                ) {
1261                (Tuple9::_T9{_0, _1, _2, _3, _4, _5, _6, _7, _8, }, Tuple9::_T9{_0: _2__0, _1: _2__1, _2: _2__2, _3: _2__3, _4: _2__4, _5: _2__5, _6: _2__6, _7: _2__7, _8: _2__8, }) => {
1262                    _0 == _2__0 && _1 == _2__1 && _2 == _2__2 && _3 == _2__3 && _4 == _2__4 && _5 == _2__5 && _6 == _2__6 && _7 == _2__7 && _8 == _2__8
1263                },
1264                _ => {
1265                    false
1266                },
1267            }
1268        }
1269    }
1270
1271    impl<T0: DafnyType + Eq + Hash, T1: DafnyType + Eq + Hash, T2: DafnyType + Eq + Hash, T3: DafnyType + Eq + Hash, T4: DafnyType + Eq + Hash, T5: DafnyType + Eq + Hash, T6: DafnyType + Eq + Hash, T7: DafnyType + Eq + Hash, T8: DafnyType + Eq + Hash> Eq
1272        for Tuple9<T0, T1, T2, T3, T4, T5, T6, T7, T8> {}
1273
1274    impl<T0: DafnyType + Hash, T1: DafnyType + Hash, T2: DafnyType + Hash, T3: DafnyType + Hash, T4: DafnyType + Hash, T5: DafnyType + Hash, T6: DafnyType + Hash, T7: DafnyType + Hash, T8: DafnyType + Hash> Hash
1275        for Tuple9<T0, T1, T2, T3, T4, T5, T6, T7, T8> {
1276        fn hash<_H: Hasher>(&self, _state: &mut _H) {
1277            match self {
1278                Tuple9::_T9{_0, _1, _2, _3, _4, _5, _6, _7, _8, } => {
1279                    Hash::hash(_0, _state);
1280                    Hash::hash(_1, _state);
1281                    Hash::hash(_2, _state);
1282                    Hash::hash(_3, _state);
1283                    Hash::hash(_4, _state);
1284                    Hash::hash(_5, _state);
1285                    Hash::hash(_6, _state);
1286                    Hash::hash(_7, _state);
1287                    Hash::hash(_8, _state)
1288                },
1289            }
1290        }
1291    }
1292
1293    impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType> AsRef<Tuple9<T0, T1, T2, T3, T4, T5, T6, T7, T8>>
1294        for Tuple9<T0, T1, T2, T3, T4, T5, T6, T7, T8> {
1295        fn as_ref(&self) -> &Self {
1296            self
1297        }
1298    }
1299
1300    #[derive(Clone)]
1301    pub enum Tuple10<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType, T9: DafnyType> {
1302        _T10 {
1303            _0: T0,
1304            _1: T1,
1305            _2: T2,
1306            _3: T3,
1307            _4: T4,
1308            _5: T5,
1309            _6: T6,
1310            _7: T7,
1311            _8: T8,
1312            _9: T9
1313        }
1314    }
1315
1316    impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType, T9: DafnyType> Tuple10<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9> {
1317        /// Returns a borrow of the field _0
1318        pub fn _0(&self) -> &T0 {
1319            match self {
1320                Tuple10::_T10{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, } => _0,
1321            }
1322        }
1323        /// Returns a borrow of the field _1
1324        pub fn _1(&self) -> &T1 {
1325            match self {
1326                Tuple10::_T10{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, } => _1,
1327            }
1328        }
1329        /// Returns a borrow of the field _2
1330        pub fn _2(&self) -> &T2 {
1331            match self {
1332                Tuple10::_T10{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, } => _2,
1333            }
1334        }
1335        /// Returns a borrow of the field _3
1336        pub fn _3(&self) -> &T3 {
1337            match self {
1338                Tuple10::_T10{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, } => _3,
1339            }
1340        }
1341        /// Returns a borrow of the field _4
1342        pub fn _4(&self) -> &T4 {
1343            match self {
1344                Tuple10::_T10{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, } => _4,
1345            }
1346        }
1347        /// Returns a borrow of the field _5
1348        pub fn _5(&self) -> &T5 {
1349            match self {
1350                Tuple10::_T10{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, } => _5,
1351            }
1352        }
1353        /// Returns a borrow of the field _6
1354        pub fn _6(&self) -> &T6 {
1355            match self {
1356                Tuple10::_T10{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, } => _6,
1357            }
1358        }
1359        /// Returns a borrow of the field _7
1360        pub fn _7(&self) -> &T7 {
1361            match self {
1362                Tuple10::_T10{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, } => _7,
1363            }
1364        }
1365        /// Returns a borrow of the field _8
1366        pub fn _8(&self) -> &T8 {
1367            match self {
1368                Tuple10::_T10{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, } => _8,
1369            }
1370        }
1371        /// Returns a borrow of the field _9
1372        pub fn _9(&self) -> &T9 {
1373            match self {
1374                Tuple10::_T10{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, } => _9,
1375            }
1376        }
1377    }
1378
1379    impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType, T9: DafnyType> Debug
1380        for Tuple10<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9> {
1381        fn fmt(&self, f: &mut Formatter) -> Result {
1382            DafnyPrint::fmt_print(self, f, true)
1383        }
1384    }
1385
1386    impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType, T9: DafnyType> DafnyPrint
1387        for Tuple10<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9> {
1388        fn fmt_print(&self, _formatter: &mut Formatter, _in_seq: bool) -> std::fmt::Result {
1389            match self {
1390                Tuple10::_T10{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, } => {
1391                    write!(_formatter, "(")?;
1392                    DafnyPrint::fmt_print(_0, _formatter, false)?;
1393                    write!(_formatter, ", ")?;
1394                    DafnyPrint::fmt_print(_1, _formatter, false)?;
1395                    write!(_formatter, ", ")?;
1396                    DafnyPrint::fmt_print(_2, _formatter, false)?;
1397                    write!(_formatter, ", ")?;
1398                    DafnyPrint::fmt_print(_3, _formatter, false)?;
1399                    write!(_formatter, ", ")?;
1400                    DafnyPrint::fmt_print(_4, _formatter, false)?;
1401                    write!(_formatter, ", ")?;
1402                    DafnyPrint::fmt_print(_5, _formatter, false)?;
1403                    write!(_formatter, ", ")?;
1404                    DafnyPrint::fmt_print(_6, _formatter, false)?;
1405                    write!(_formatter, ", ")?;
1406                    DafnyPrint::fmt_print(_7, _formatter, false)?;
1407                    write!(_formatter, ", ")?;
1408                    DafnyPrint::fmt_print(_8, _formatter, false)?;
1409                    write!(_formatter, ", ")?;
1410                    DafnyPrint::fmt_print(_9, _formatter, false)?;
1411                    write!(_formatter, ")")?;
1412                    Ok(())
1413                },
1414            }
1415        }
1416    }
1417
1418    impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType, T9: DafnyType> Tuple10<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9> {
1419        /// Given type parameter conversions, returns a lambda to convert this structure
1420        pub fn coerce<__T0: DafnyType, __T1: DafnyType, __T2: DafnyType, __T3: DafnyType, __T4: DafnyType, __T5: DafnyType, __T6: DafnyType, __T7: DafnyType, __T8: DafnyType, __T9: DafnyType>(f_0: Rc<impl ::std::ops::Fn(T0) -> __T0 + 'static>, f_1: Rc<impl ::std::ops::Fn(T1) -> __T1 + 'static>, f_2: Rc<impl ::std::ops::Fn(T2) -> __T2 + 'static>, f_3: Rc<impl ::std::ops::Fn(T3) -> __T3 + 'static>, f_4: Rc<impl ::std::ops::Fn(T4) -> __T4 + 'static>, f_5: Rc<impl ::std::ops::Fn(T5) -> __T5 + 'static>, f_6: Rc<impl ::std::ops::Fn(T6) -> __T6 + 'static>, f_7: Rc<impl ::std::ops::Fn(T7) -> __T7 + 'static>, f_8: Rc<impl ::std::ops::Fn(T8) -> __T8 + 'static>, f_9: Rc<impl ::std::ops::Fn(T9) -> __T9 + 'static>) -> Rc<impl ::std::ops::Fn(Tuple10<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9>) -> Tuple10<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8, __T9>> {
1421            Rc::new(move |this: Self| -> Tuple10<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8, __T9>{
1422                    match this {
1423                        Tuple10::_T10{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, } => {
1424                            Tuple10::_T10 {
1425                                _0: f_0.clone()(_0),
1426                                _1: f_1.clone()(_1),
1427                                _2: f_2.clone()(_2),
1428                                _3: f_3.clone()(_3),
1429                                _4: f_4.clone()(_4),
1430                                _5: f_5.clone()(_5),
1431                                _6: f_6.clone()(_6),
1432                                _7: f_7.clone()(_7),
1433                                _8: f_8.clone()(_8),
1434                                _9: f_9.clone()(_9)
1435                            }
1436                        },
1437                    }
1438                })
1439        }
1440    }
1441
1442    impl<T0: DafnyType + Eq + Hash, T1: DafnyType + Eq + Hash, T2: DafnyType + Eq + Hash, T3: DafnyType + Eq + Hash, T4: DafnyType + Eq + Hash, T5: DafnyType + Eq + Hash, T6: DafnyType + Eq + Hash, T7: DafnyType + Eq + Hash, T8: DafnyType + Eq + Hash, T9: DafnyType + Eq + Hash> PartialEq
1443        for Tuple10<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9> {
1444        fn eq(&self, other: &Self) -> bool {
1445            match (
1446                    self,
1447                    other
1448                ) {
1449                (Tuple10::_T10{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, }, Tuple10::_T10{_0: _2__0, _1: _2__1, _2: _2__2, _3: _2__3, _4: _2__4, _5: _2__5, _6: _2__6, _7: _2__7, _8: _2__8, _9: _2__9, }) => {
1450                    _0 == _2__0 && _1 == _2__1 && _2 == _2__2 && _3 == _2__3 && _4 == _2__4 && _5 == _2__5 && _6 == _2__6 && _7 == _2__7 && _8 == _2__8 && _9 == _2__9
1451                },
1452                _ => {
1453                    false
1454                },
1455            }
1456        }
1457    }
1458
1459    impl<T0: DafnyType + Eq + Hash, T1: DafnyType + Eq + Hash, T2: DafnyType + Eq + Hash, T3: DafnyType + Eq + Hash, T4: DafnyType + Eq + Hash, T5: DafnyType + Eq + Hash, T6: DafnyType + Eq + Hash, T7: DafnyType + Eq + Hash, T8: DafnyType + Eq + Hash, T9: DafnyType + Eq + Hash> Eq
1460        for Tuple10<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9> {}
1461
1462    impl<T0: DafnyType + Hash, T1: DafnyType + Hash, T2: DafnyType + Hash, T3: DafnyType + Hash, T4: DafnyType + Hash, T5: DafnyType + Hash, T6: DafnyType + Hash, T7: DafnyType + Hash, T8: DafnyType + Hash, T9: DafnyType + Hash> Hash
1463        for Tuple10<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9> {
1464        fn hash<_H: Hasher>(&self, _state: &mut _H) {
1465            match self {
1466                Tuple10::_T10{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, } => {
1467                    Hash::hash(_0, _state);
1468                    Hash::hash(_1, _state);
1469                    Hash::hash(_2, _state);
1470                    Hash::hash(_3, _state);
1471                    Hash::hash(_4, _state);
1472                    Hash::hash(_5, _state);
1473                    Hash::hash(_6, _state);
1474                    Hash::hash(_7, _state);
1475                    Hash::hash(_8, _state);
1476                    Hash::hash(_9, _state)
1477                },
1478            }
1479        }
1480    }
1481
1482    impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType, T9: DafnyType> AsRef<Tuple10<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9>>
1483        for Tuple10<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9> {
1484        fn as_ref(&self) -> &Self {
1485            self
1486        }
1487    }
1488
1489    #[derive(Clone)]
1490    pub enum Tuple11<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType, T9: DafnyType, T10: DafnyType> {
1491        _T11 {
1492            _0: T0,
1493            _1: T1,
1494            _2: T2,
1495            _3: T3,
1496            _4: T4,
1497            _5: T5,
1498            _6: T6,
1499            _7: T7,
1500            _8: T8,
1501            _9: T9,
1502            _10: T10
1503        }
1504    }
1505
1506    impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType, T9: DafnyType, T10: DafnyType> Tuple11<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10> {
1507        /// Returns a borrow of the field _0
1508        pub fn _0(&self) -> &T0 {
1509            match self {
1510                Tuple11::_T11{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, } => _0,
1511            }
1512        }
1513        /// Returns a borrow of the field _1
1514        pub fn _1(&self) -> &T1 {
1515            match self {
1516                Tuple11::_T11{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, } => _1,
1517            }
1518        }
1519        /// Returns a borrow of the field _2
1520        pub fn _2(&self) -> &T2 {
1521            match self {
1522                Tuple11::_T11{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, } => _2,
1523            }
1524        }
1525        /// Returns a borrow of the field _3
1526        pub fn _3(&self) -> &T3 {
1527            match self {
1528                Tuple11::_T11{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, } => _3,
1529            }
1530        }
1531        /// Returns a borrow of the field _4
1532        pub fn _4(&self) -> &T4 {
1533            match self {
1534                Tuple11::_T11{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, } => _4,
1535            }
1536        }
1537        /// Returns a borrow of the field _5
1538        pub fn _5(&self) -> &T5 {
1539            match self {
1540                Tuple11::_T11{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, } => _5,
1541            }
1542        }
1543        /// Returns a borrow of the field _6
1544        pub fn _6(&self) -> &T6 {
1545            match self {
1546                Tuple11::_T11{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, } => _6,
1547            }
1548        }
1549        /// Returns a borrow of the field _7
1550        pub fn _7(&self) -> &T7 {
1551            match self {
1552                Tuple11::_T11{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, } => _7,
1553            }
1554        }
1555        /// Returns a borrow of the field _8
1556        pub fn _8(&self) -> &T8 {
1557            match self {
1558                Tuple11::_T11{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, } => _8,
1559            }
1560        }
1561        /// Returns a borrow of the field _9
1562        pub fn _9(&self) -> &T9 {
1563            match self {
1564                Tuple11::_T11{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, } => _9,
1565            }
1566        }
1567        /// Returns a borrow of the field _10
1568        pub fn _10(&self) -> &T10 {
1569            match self {
1570                Tuple11::_T11{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, } => _10,
1571            }
1572        }
1573    }
1574
1575    impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType, T9: DafnyType, T10: DafnyType> Debug
1576        for Tuple11<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10> {
1577        fn fmt(&self, f: &mut Formatter) -> Result {
1578            DafnyPrint::fmt_print(self, f, true)
1579        }
1580    }
1581
1582    impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType, T9: DafnyType, T10: DafnyType> DafnyPrint
1583        for Tuple11<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10> {
1584        fn fmt_print(&self, _formatter: &mut Formatter, _in_seq: bool) -> std::fmt::Result {
1585            match self {
1586                Tuple11::_T11{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, } => {
1587                    write!(_formatter, "(")?;
1588                    DafnyPrint::fmt_print(_0, _formatter, false)?;
1589                    write!(_formatter, ", ")?;
1590                    DafnyPrint::fmt_print(_1, _formatter, false)?;
1591                    write!(_formatter, ", ")?;
1592                    DafnyPrint::fmt_print(_2, _formatter, false)?;
1593                    write!(_formatter, ", ")?;
1594                    DafnyPrint::fmt_print(_3, _formatter, false)?;
1595                    write!(_formatter, ", ")?;
1596                    DafnyPrint::fmt_print(_4, _formatter, false)?;
1597                    write!(_formatter, ", ")?;
1598                    DafnyPrint::fmt_print(_5, _formatter, false)?;
1599                    write!(_formatter, ", ")?;
1600                    DafnyPrint::fmt_print(_6, _formatter, false)?;
1601                    write!(_formatter, ", ")?;
1602                    DafnyPrint::fmt_print(_7, _formatter, false)?;
1603                    write!(_formatter, ", ")?;
1604                    DafnyPrint::fmt_print(_8, _formatter, false)?;
1605                    write!(_formatter, ", ")?;
1606                    DafnyPrint::fmt_print(_9, _formatter, false)?;
1607                    write!(_formatter, ", ")?;
1608                    DafnyPrint::fmt_print(_10, _formatter, false)?;
1609                    write!(_formatter, ")")?;
1610                    Ok(())
1611                },
1612            }
1613        }
1614    }
1615
1616    impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType, T9: DafnyType, T10: DafnyType> Tuple11<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10> {
1617        /// Given type parameter conversions, returns a lambda to convert this structure
1618        pub fn coerce<__T0: DafnyType, __T1: DafnyType, __T2: DafnyType, __T3: DafnyType, __T4: DafnyType, __T5: DafnyType, __T6: DafnyType, __T7: DafnyType, __T8: DafnyType, __T9: DafnyType, __T10: DafnyType>(f_0: Rc<impl ::std::ops::Fn(T0) -> __T0 + 'static>, f_1: Rc<impl ::std::ops::Fn(T1) -> __T1 + 'static>, f_2: Rc<impl ::std::ops::Fn(T2) -> __T2 + 'static>, f_3: Rc<impl ::std::ops::Fn(T3) -> __T3 + 'static>, f_4: Rc<impl ::std::ops::Fn(T4) -> __T4 + 'static>, f_5: Rc<impl ::std::ops::Fn(T5) -> __T5 + 'static>, f_6: Rc<impl ::std::ops::Fn(T6) -> __T6 + 'static>, f_7: Rc<impl ::std::ops::Fn(T7) -> __T7 + 'static>, f_8: Rc<impl ::std::ops::Fn(T8) -> __T8 + 'static>, f_9: Rc<impl ::std::ops::Fn(T9) -> __T9 + 'static>, f_10: Rc<impl ::std::ops::Fn(T10) -> __T10 + 'static>) -> Rc<impl ::std::ops::Fn(Tuple11<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10>) -> Tuple11<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8, __T9, __T10>> {
1619            Rc::new(move |this: Self| -> Tuple11<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8, __T9, __T10>{
1620                    match this {
1621                        Tuple11::_T11{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, } => {
1622                            Tuple11::_T11 {
1623                                _0: f_0.clone()(_0),
1624                                _1: f_1.clone()(_1),
1625                                _2: f_2.clone()(_2),
1626                                _3: f_3.clone()(_3),
1627                                _4: f_4.clone()(_4),
1628                                _5: f_5.clone()(_5),
1629                                _6: f_6.clone()(_6),
1630                                _7: f_7.clone()(_7),
1631                                _8: f_8.clone()(_8),
1632                                _9: f_9.clone()(_9),
1633                                _10: f_10.clone()(_10)
1634                            }
1635                        },
1636                    }
1637                })
1638        }
1639    }
1640
1641    impl<T0: DafnyType + Eq + Hash, T1: DafnyType + Eq + Hash, T2: DafnyType + Eq + Hash, T3: DafnyType + Eq + Hash, T4: DafnyType + Eq + Hash, T5: DafnyType + Eq + Hash, T6: DafnyType + Eq + Hash, T7: DafnyType + Eq + Hash, T8: DafnyType + Eq + Hash, T9: DafnyType + Eq + Hash, T10: DafnyType + Eq + Hash> PartialEq
1642        for Tuple11<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10> {
1643        fn eq(&self, other: &Self) -> bool {
1644            match (
1645                    self,
1646                    other
1647                ) {
1648                (Tuple11::_T11{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, }, Tuple11::_T11{_0: _2__0, _1: _2__1, _2: _2__2, _3: _2__3, _4: _2__4, _5: _2__5, _6: _2__6, _7: _2__7, _8: _2__8, _9: _2__9, _10: _2__10, }) => {
1649                    _0 == _2__0 && _1 == _2__1 && _2 == _2__2 && _3 == _2__3 && _4 == _2__4 && _5 == _2__5 && _6 == _2__6 && _7 == _2__7 && _8 == _2__8 && _9 == _2__9 && _10 == _2__10
1650                },
1651                _ => {
1652                    false
1653                },
1654            }
1655        }
1656    }
1657
1658    impl<T0: DafnyType + Eq + Hash, T1: DafnyType + Eq + Hash, T2: DafnyType + Eq + Hash, T3: DafnyType + Eq + Hash, T4: DafnyType + Eq + Hash, T5: DafnyType + Eq + Hash, T6: DafnyType + Eq + Hash, T7: DafnyType + Eq + Hash, T8: DafnyType + Eq + Hash, T9: DafnyType + Eq + Hash, T10: DafnyType + Eq + Hash> Eq
1659        for Tuple11<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10> {}
1660
1661    impl<T0: DafnyType + Hash, T1: DafnyType + Hash, T2: DafnyType + Hash, T3: DafnyType + Hash, T4: DafnyType + Hash, T5: DafnyType + Hash, T6: DafnyType + Hash, T7: DafnyType + Hash, T8: DafnyType + Hash, T9: DafnyType + Hash, T10: DafnyType + Hash> Hash
1662        for Tuple11<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10> {
1663        fn hash<_H: Hasher>(&self, _state: &mut _H) {
1664            match self {
1665                Tuple11::_T11{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, } => {
1666                    Hash::hash(_0, _state);
1667                    Hash::hash(_1, _state);
1668                    Hash::hash(_2, _state);
1669                    Hash::hash(_3, _state);
1670                    Hash::hash(_4, _state);
1671                    Hash::hash(_5, _state);
1672                    Hash::hash(_6, _state);
1673                    Hash::hash(_7, _state);
1674                    Hash::hash(_8, _state);
1675                    Hash::hash(_9, _state);
1676                    Hash::hash(_10, _state)
1677                },
1678            }
1679        }
1680    }
1681
1682    impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType, T9: DafnyType, T10: DafnyType> AsRef<Tuple11<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10>>
1683        for Tuple11<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10> {
1684        fn as_ref(&self) -> &Self {
1685            self
1686        }
1687    }
1688
1689    #[derive(Clone)]
1690    pub enum Tuple12<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType, T9: DafnyType, T10: DafnyType, T11: DafnyType> {
1691        _T12 {
1692            _0: T0,
1693            _1: T1,
1694            _2: T2,
1695            _3: T3,
1696            _4: T4,
1697            _5: T5,
1698            _6: T6,
1699            _7: T7,
1700            _8: T8,
1701            _9: T9,
1702            _10: T10,
1703            _11: T11
1704        }
1705    }
1706
1707    impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType, T9: DafnyType, T10: DafnyType, T11: DafnyType> Tuple12<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11> {
1708        /// Returns a borrow of the field _0
1709        pub fn _0(&self) -> &T0 {
1710            match self {
1711                Tuple12::_T12{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, } => _0,
1712            }
1713        }
1714        /// Returns a borrow of the field _1
1715        pub fn _1(&self) -> &T1 {
1716            match self {
1717                Tuple12::_T12{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, } => _1,
1718            }
1719        }
1720        /// Returns a borrow of the field _2
1721        pub fn _2(&self) -> &T2 {
1722            match self {
1723                Tuple12::_T12{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, } => _2,
1724            }
1725        }
1726        /// Returns a borrow of the field _3
1727        pub fn _3(&self) -> &T3 {
1728            match self {
1729                Tuple12::_T12{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, } => _3,
1730            }
1731        }
1732        /// Returns a borrow of the field _4
1733        pub fn _4(&self) -> &T4 {
1734            match self {
1735                Tuple12::_T12{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, } => _4,
1736            }
1737        }
1738        /// Returns a borrow of the field _5
1739        pub fn _5(&self) -> &T5 {
1740            match self {
1741                Tuple12::_T12{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, } => _5,
1742            }
1743        }
1744        /// Returns a borrow of the field _6
1745        pub fn _6(&self) -> &T6 {
1746            match self {
1747                Tuple12::_T12{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, } => _6,
1748            }
1749        }
1750        /// Returns a borrow of the field _7
1751        pub fn _7(&self) -> &T7 {
1752            match self {
1753                Tuple12::_T12{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, } => _7,
1754            }
1755        }
1756        /// Returns a borrow of the field _8
1757        pub fn _8(&self) -> &T8 {
1758            match self {
1759                Tuple12::_T12{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, } => _8,
1760            }
1761        }
1762        /// Returns a borrow of the field _9
1763        pub fn _9(&self) -> &T9 {
1764            match self {
1765                Tuple12::_T12{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, } => _9,
1766            }
1767        }
1768        /// Returns a borrow of the field _10
1769        pub fn _10(&self) -> &T10 {
1770            match self {
1771                Tuple12::_T12{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, } => _10,
1772            }
1773        }
1774        /// Returns a borrow of the field _11
1775        pub fn _11(&self) -> &T11 {
1776            match self {
1777                Tuple12::_T12{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, } => _11,
1778            }
1779        }
1780    }
1781
1782    impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType, T9: DafnyType, T10: DafnyType, T11: DafnyType> Debug
1783        for Tuple12<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11> {
1784        fn fmt(&self, f: &mut Formatter) -> Result {
1785            DafnyPrint::fmt_print(self, f, true)
1786        }
1787    }
1788
1789    impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType, T9: DafnyType, T10: DafnyType, T11: DafnyType> DafnyPrint
1790        for Tuple12<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11> {
1791        fn fmt_print(&self, _formatter: &mut Formatter, _in_seq: bool) -> std::fmt::Result {
1792            match self {
1793                Tuple12::_T12{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, } => {
1794                    write!(_formatter, "(")?;
1795                    DafnyPrint::fmt_print(_0, _formatter, false)?;
1796                    write!(_formatter, ", ")?;
1797                    DafnyPrint::fmt_print(_1, _formatter, false)?;
1798                    write!(_formatter, ", ")?;
1799                    DafnyPrint::fmt_print(_2, _formatter, false)?;
1800                    write!(_formatter, ", ")?;
1801                    DafnyPrint::fmt_print(_3, _formatter, false)?;
1802                    write!(_formatter, ", ")?;
1803                    DafnyPrint::fmt_print(_4, _formatter, false)?;
1804                    write!(_formatter, ", ")?;
1805                    DafnyPrint::fmt_print(_5, _formatter, false)?;
1806                    write!(_formatter, ", ")?;
1807                    DafnyPrint::fmt_print(_6, _formatter, false)?;
1808                    write!(_formatter, ", ")?;
1809                    DafnyPrint::fmt_print(_7, _formatter, false)?;
1810                    write!(_formatter, ", ")?;
1811                    DafnyPrint::fmt_print(_8, _formatter, false)?;
1812                    write!(_formatter, ", ")?;
1813                    DafnyPrint::fmt_print(_9, _formatter, false)?;
1814                    write!(_formatter, ", ")?;
1815                    DafnyPrint::fmt_print(_10, _formatter, false)?;
1816                    write!(_formatter, ", ")?;
1817                    DafnyPrint::fmt_print(_11, _formatter, false)?;
1818                    write!(_formatter, ")")?;
1819                    Ok(())
1820                },
1821            }
1822        }
1823    }
1824
1825    impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType, T9: DafnyType, T10: DafnyType, T11: DafnyType> Tuple12<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11> {
1826        /// Given type parameter conversions, returns a lambda to convert this structure
1827        pub fn coerce<__T0: DafnyType, __T1: DafnyType, __T2: DafnyType, __T3: DafnyType, __T4: DafnyType, __T5: DafnyType, __T6: DafnyType, __T7: DafnyType, __T8: DafnyType, __T9: DafnyType, __T10: DafnyType, __T11: DafnyType>(f_0: Rc<impl ::std::ops::Fn(T0) -> __T0 + 'static>, f_1: Rc<impl ::std::ops::Fn(T1) -> __T1 + 'static>, f_2: Rc<impl ::std::ops::Fn(T2) -> __T2 + 'static>, f_3: Rc<impl ::std::ops::Fn(T3) -> __T3 + 'static>, f_4: Rc<impl ::std::ops::Fn(T4) -> __T4 + 'static>, f_5: Rc<impl ::std::ops::Fn(T5) -> __T5 + 'static>, f_6: Rc<impl ::std::ops::Fn(T6) -> __T6 + 'static>, f_7: Rc<impl ::std::ops::Fn(T7) -> __T7 + 'static>, f_8: Rc<impl ::std::ops::Fn(T8) -> __T8 + 'static>, f_9: Rc<impl ::std::ops::Fn(T9) -> __T9 + 'static>, f_10: Rc<impl ::std::ops::Fn(T10) -> __T10 + 'static>, f_11: Rc<impl ::std::ops::Fn(T11) -> __T11 + 'static>) -> Rc<impl ::std::ops::Fn(Tuple12<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11>) -> Tuple12<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8, __T9, __T10, __T11>> {
1828            Rc::new(move |this: Self| -> Tuple12<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8, __T9, __T10, __T11>{
1829                    match this {
1830                        Tuple12::_T12{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, } => {
1831                            Tuple12::_T12 {
1832                                _0: f_0.clone()(_0),
1833                                _1: f_1.clone()(_1),
1834                                _2: f_2.clone()(_2),
1835                                _3: f_3.clone()(_3),
1836                                _4: f_4.clone()(_4),
1837                                _5: f_5.clone()(_5),
1838                                _6: f_6.clone()(_6),
1839                                _7: f_7.clone()(_7),
1840                                _8: f_8.clone()(_8),
1841                                _9: f_9.clone()(_9),
1842                                _10: f_10.clone()(_10),
1843                                _11: f_11.clone()(_11)
1844                            }
1845                        },
1846                    }
1847                })
1848        }
1849    }
1850
1851    impl<T0: DafnyType + Eq + Hash, T1: DafnyType + Eq + Hash, T2: DafnyType + Eq + Hash, T3: DafnyType + Eq + Hash, T4: DafnyType + Eq + Hash, T5: DafnyType + Eq + Hash, T6: DafnyType + Eq + Hash, T7: DafnyType + Eq + Hash, T8: DafnyType + Eq + Hash, T9: DafnyType + Eq + Hash, T10: DafnyType + Eq + Hash, T11: DafnyType + Eq + Hash> PartialEq
1852        for Tuple12<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11> {
1853        fn eq(&self, other: &Self) -> bool {
1854            match (
1855                    self,
1856                    other
1857                ) {
1858                (Tuple12::_T12{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, }, Tuple12::_T12{_0: _2__0, _1: _2__1, _2: _2__2, _3: _2__3, _4: _2__4, _5: _2__5, _6: _2__6, _7: _2__7, _8: _2__8, _9: _2__9, _10: _2__10, _11: _2__11, }) => {
1859                    _0 == _2__0 && _1 == _2__1 && _2 == _2__2 && _3 == _2__3 && _4 == _2__4 && _5 == _2__5 && _6 == _2__6 && _7 == _2__7 && _8 == _2__8 && _9 == _2__9 && _10 == _2__10 && _11 == _2__11
1860                },
1861                _ => {
1862                    false
1863                },
1864            }
1865        }
1866    }
1867
1868    impl<T0: DafnyType + Eq + Hash, T1: DafnyType + Eq + Hash, T2: DafnyType + Eq + Hash, T3: DafnyType + Eq + Hash, T4: DafnyType + Eq + Hash, T5: DafnyType + Eq + Hash, T6: DafnyType + Eq + Hash, T7: DafnyType + Eq + Hash, T8: DafnyType + Eq + Hash, T9: DafnyType + Eq + Hash, T10: DafnyType + Eq + Hash, T11: DafnyType + Eq + Hash> Eq
1869        for Tuple12<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11> {}
1870
1871    impl<T0: DafnyType + Hash, T1: DafnyType + Hash, T2: DafnyType + Hash, T3: DafnyType + Hash, T4: DafnyType + Hash, T5: DafnyType + Hash, T6: DafnyType + Hash, T7: DafnyType + Hash, T8: DafnyType + Hash, T9: DafnyType + Hash, T10: DafnyType + Hash, T11: DafnyType + Hash> Hash
1872        for Tuple12<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11> {
1873        fn hash<_H: Hasher>(&self, _state: &mut _H) {
1874            match self {
1875                Tuple12::_T12{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, } => {
1876                    Hash::hash(_0, _state);
1877                    Hash::hash(_1, _state);
1878                    Hash::hash(_2, _state);
1879                    Hash::hash(_3, _state);
1880                    Hash::hash(_4, _state);
1881                    Hash::hash(_5, _state);
1882                    Hash::hash(_6, _state);
1883                    Hash::hash(_7, _state);
1884                    Hash::hash(_8, _state);
1885                    Hash::hash(_9, _state);
1886                    Hash::hash(_10, _state);
1887                    Hash::hash(_11, _state)
1888                },
1889            }
1890        }
1891    }
1892
1893    impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType, T9: DafnyType, T10: DafnyType, T11: DafnyType> AsRef<Tuple12<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11>>
1894        for Tuple12<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11> {
1895        fn as_ref(&self) -> &Self {
1896            self
1897        }
1898    }
1899
1900    #[derive(Clone)]
1901    pub enum Tuple13<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType, T9: DafnyType, T10: DafnyType, T11: DafnyType, T12: DafnyType> {
1902        _T13 {
1903            _0: T0,
1904            _1: T1,
1905            _2: T2,
1906            _3: T3,
1907            _4: T4,
1908            _5: T5,
1909            _6: T6,
1910            _7: T7,
1911            _8: T8,
1912            _9: T9,
1913            _10: T10,
1914            _11: T11,
1915            _12: T12
1916        }
1917    }
1918
1919    impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType, T9: DafnyType, T10: DafnyType, T11: DafnyType, T12: DafnyType> Tuple13<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12> {
1920        /// Returns a borrow of the field _0
1921        pub fn _0(&self) -> &T0 {
1922            match self {
1923                Tuple13::_T13{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, } => _0,
1924            }
1925        }
1926        /// Returns a borrow of the field _1
1927        pub fn _1(&self) -> &T1 {
1928            match self {
1929                Tuple13::_T13{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, } => _1,
1930            }
1931        }
1932        /// Returns a borrow of the field _2
1933        pub fn _2(&self) -> &T2 {
1934            match self {
1935                Tuple13::_T13{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, } => _2,
1936            }
1937        }
1938        /// Returns a borrow of the field _3
1939        pub fn _3(&self) -> &T3 {
1940            match self {
1941                Tuple13::_T13{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, } => _3,
1942            }
1943        }
1944        /// Returns a borrow of the field _4
1945        pub fn _4(&self) -> &T4 {
1946            match self {
1947                Tuple13::_T13{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, } => _4,
1948            }
1949        }
1950        /// Returns a borrow of the field _5
1951        pub fn _5(&self) -> &T5 {
1952            match self {
1953                Tuple13::_T13{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, } => _5,
1954            }
1955        }
1956        /// Returns a borrow of the field _6
1957        pub fn _6(&self) -> &T6 {
1958            match self {
1959                Tuple13::_T13{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, } => _6,
1960            }
1961        }
1962        /// Returns a borrow of the field _7
1963        pub fn _7(&self) -> &T7 {
1964            match self {
1965                Tuple13::_T13{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, } => _7,
1966            }
1967        }
1968        /// Returns a borrow of the field _8
1969        pub fn _8(&self) -> &T8 {
1970            match self {
1971                Tuple13::_T13{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, } => _8,
1972            }
1973        }
1974        /// Returns a borrow of the field _9
1975        pub fn _9(&self) -> &T9 {
1976            match self {
1977                Tuple13::_T13{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, } => _9,
1978            }
1979        }
1980        /// Returns a borrow of the field _10
1981        pub fn _10(&self) -> &T10 {
1982            match self {
1983                Tuple13::_T13{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, } => _10,
1984            }
1985        }
1986        /// Returns a borrow of the field _11
1987        pub fn _11(&self) -> &T11 {
1988            match self {
1989                Tuple13::_T13{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, } => _11,
1990            }
1991        }
1992        /// Returns a borrow of the field _12
1993        pub fn _12(&self) -> &T12 {
1994            match self {
1995                Tuple13::_T13{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, } => _12,
1996            }
1997        }
1998    }
1999
2000    impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType, T9: DafnyType, T10: DafnyType, T11: DafnyType, T12: DafnyType> Debug
2001        for Tuple13<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12> {
2002        fn fmt(&self, f: &mut Formatter) -> Result {
2003            DafnyPrint::fmt_print(self, f, true)
2004        }
2005    }
2006
2007    impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType, T9: DafnyType, T10: DafnyType, T11: DafnyType, T12: DafnyType> DafnyPrint
2008        for Tuple13<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12> {
2009        fn fmt_print(&self, _formatter: &mut Formatter, _in_seq: bool) -> std::fmt::Result {
2010            match self {
2011                Tuple13::_T13{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, } => {
2012                    write!(_formatter, "(")?;
2013                    DafnyPrint::fmt_print(_0, _formatter, false)?;
2014                    write!(_formatter, ", ")?;
2015                    DafnyPrint::fmt_print(_1, _formatter, false)?;
2016                    write!(_formatter, ", ")?;
2017                    DafnyPrint::fmt_print(_2, _formatter, false)?;
2018                    write!(_formatter, ", ")?;
2019                    DafnyPrint::fmt_print(_3, _formatter, false)?;
2020                    write!(_formatter, ", ")?;
2021                    DafnyPrint::fmt_print(_4, _formatter, false)?;
2022                    write!(_formatter, ", ")?;
2023                    DafnyPrint::fmt_print(_5, _formatter, false)?;
2024                    write!(_formatter, ", ")?;
2025                    DafnyPrint::fmt_print(_6, _formatter, false)?;
2026                    write!(_formatter, ", ")?;
2027                    DafnyPrint::fmt_print(_7, _formatter, false)?;
2028                    write!(_formatter, ", ")?;
2029                    DafnyPrint::fmt_print(_8, _formatter, false)?;
2030                    write!(_formatter, ", ")?;
2031                    DafnyPrint::fmt_print(_9, _formatter, false)?;
2032                    write!(_formatter, ", ")?;
2033                    DafnyPrint::fmt_print(_10, _formatter, false)?;
2034                    write!(_formatter, ", ")?;
2035                    DafnyPrint::fmt_print(_11, _formatter, false)?;
2036                    write!(_formatter, ", ")?;
2037                    DafnyPrint::fmt_print(_12, _formatter, false)?;
2038                    write!(_formatter, ")")?;
2039                    Ok(())
2040                },
2041            }
2042        }
2043    }
2044
2045    impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType, T9: DafnyType, T10: DafnyType, T11: DafnyType, T12: DafnyType> Tuple13<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12> {
2046        /// Given type parameter conversions, returns a lambda to convert this structure
2047        pub fn coerce<__T0: DafnyType, __T1: DafnyType, __T2: DafnyType, __T3: DafnyType, __T4: DafnyType, __T5: DafnyType, __T6: DafnyType, __T7: DafnyType, __T8: DafnyType, __T9: DafnyType, __T10: DafnyType, __T11: DafnyType, __T12: DafnyType>(f_0: Rc<impl ::std::ops::Fn(T0) -> __T0 + 'static>, f_1: Rc<impl ::std::ops::Fn(T1) -> __T1 + 'static>, f_2: Rc<impl ::std::ops::Fn(T2) -> __T2 + 'static>, f_3: Rc<impl ::std::ops::Fn(T3) -> __T3 + 'static>, f_4: Rc<impl ::std::ops::Fn(T4) -> __T4 + 'static>, f_5: Rc<impl ::std::ops::Fn(T5) -> __T5 + 'static>, f_6: Rc<impl ::std::ops::Fn(T6) -> __T6 + 'static>, f_7: Rc<impl ::std::ops::Fn(T7) -> __T7 + 'static>, f_8: Rc<impl ::std::ops::Fn(T8) -> __T8 + 'static>, f_9: Rc<impl ::std::ops::Fn(T9) -> __T9 + 'static>, f_10: Rc<impl ::std::ops::Fn(T10) -> __T10 + 'static>, f_11: Rc<impl ::std::ops::Fn(T11) -> __T11 + 'static>, f_12: Rc<impl ::std::ops::Fn(T12) -> __T12 + 'static>) -> Rc<impl ::std::ops::Fn(Tuple13<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12>) -> Tuple13<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8, __T9, __T10, __T11, __T12>> {
2048            Rc::new(move |this: Self| -> Tuple13<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8, __T9, __T10, __T11, __T12>{
2049                    match this {
2050                        Tuple13::_T13{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, } => {
2051                            Tuple13::_T13 {
2052                                _0: f_0.clone()(_0),
2053                                _1: f_1.clone()(_1),
2054                                _2: f_2.clone()(_2),
2055                                _3: f_3.clone()(_3),
2056                                _4: f_4.clone()(_4),
2057                                _5: f_5.clone()(_5),
2058                                _6: f_6.clone()(_6),
2059                                _7: f_7.clone()(_7),
2060                                _8: f_8.clone()(_8),
2061                                _9: f_9.clone()(_9),
2062                                _10: f_10.clone()(_10),
2063                                _11: f_11.clone()(_11),
2064                                _12: f_12.clone()(_12)
2065                            }
2066                        },
2067                    }
2068                })
2069        }
2070    }
2071
2072    impl<T0: DafnyType + Eq + Hash, T1: DafnyType + Eq + Hash, T2: DafnyType + Eq + Hash, T3: DafnyType + Eq + Hash, T4: DafnyType + Eq + Hash, T5: DafnyType + Eq + Hash, T6: DafnyType + Eq + Hash, T7: DafnyType + Eq + Hash, T8: DafnyType + Eq + Hash, T9: DafnyType + Eq + Hash, T10: DafnyType + Eq + Hash, T11: DafnyType + Eq + Hash, T12: DafnyType + Eq + Hash> PartialEq
2073        for Tuple13<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12> {
2074        fn eq(&self, other: &Self) -> bool {
2075            match (
2076                    self,
2077                    other
2078                ) {
2079                (Tuple13::_T13{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, }, Tuple13::_T13{_0: _2__0, _1: _2__1, _2: _2__2, _3: _2__3, _4: _2__4, _5: _2__5, _6: _2__6, _7: _2__7, _8: _2__8, _9: _2__9, _10: _2__10, _11: _2__11, _12: _2__12, }) => {
2080                    _0 == _2__0 && _1 == _2__1 && _2 == _2__2 && _3 == _2__3 && _4 == _2__4 && _5 == _2__5 && _6 == _2__6 && _7 == _2__7 && _8 == _2__8 && _9 == _2__9 && _10 == _2__10 && _11 == _2__11 && _12 == _2__12
2081                },
2082                _ => {
2083                    false
2084                },
2085            }
2086        }
2087    }
2088
2089    impl<T0: DafnyType + Eq + Hash, T1: DafnyType + Eq + Hash, T2: DafnyType + Eq + Hash, T3: DafnyType + Eq + Hash, T4: DafnyType + Eq + Hash, T5: DafnyType + Eq + Hash, T6: DafnyType + Eq + Hash, T7: DafnyType + Eq + Hash, T8: DafnyType + Eq + Hash, T9: DafnyType + Eq + Hash, T10: DafnyType + Eq + Hash, T11: DafnyType + Eq + Hash, T12: DafnyType + Eq + Hash> Eq
2090        for Tuple13<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12> {}
2091
2092    impl<T0: DafnyType + Hash, T1: DafnyType + Hash, T2: DafnyType + Hash, T3: DafnyType + Hash, T4: DafnyType + Hash, T5: DafnyType + Hash, T6: DafnyType + Hash, T7: DafnyType + Hash, T8: DafnyType + Hash, T9: DafnyType + Hash, T10: DafnyType + Hash, T11: DafnyType + Hash, T12: DafnyType + Hash> Hash
2093        for Tuple13<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12> {
2094        fn hash<_H: Hasher>(&self, _state: &mut _H) {
2095            match self {
2096                Tuple13::_T13{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, } => {
2097                    Hash::hash(_0, _state);
2098                    Hash::hash(_1, _state);
2099                    Hash::hash(_2, _state);
2100                    Hash::hash(_3, _state);
2101                    Hash::hash(_4, _state);
2102                    Hash::hash(_5, _state);
2103                    Hash::hash(_6, _state);
2104                    Hash::hash(_7, _state);
2105                    Hash::hash(_8, _state);
2106                    Hash::hash(_9, _state);
2107                    Hash::hash(_10, _state);
2108                    Hash::hash(_11, _state);
2109                    Hash::hash(_12, _state)
2110                },
2111            }
2112        }
2113    }
2114
2115    impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType, T9: DafnyType, T10: DafnyType, T11: DafnyType, T12: DafnyType> AsRef<Tuple13<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12>>
2116        for Tuple13<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12> {
2117        fn as_ref(&self) -> &Self {
2118            self
2119        }
2120    }
2121
2122    #[derive(Clone)]
2123    pub enum Tuple14<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType, T9: DafnyType, T10: DafnyType, T11: DafnyType, T12: DafnyType, T13: DafnyType> {
2124        _T14 {
2125            _0: T0,
2126            _1: T1,
2127            _2: T2,
2128            _3: T3,
2129            _4: T4,
2130            _5: T5,
2131            _6: T6,
2132            _7: T7,
2133            _8: T8,
2134            _9: T9,
2135            _10: T10,
2136            _11: T11,
2137            _12: T12,
2138            _13: T13
2139        }
2140    }
2141
2142    impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType, T9: DafnyType, T10: DafnyType, T11: DafnyType, T12: DafnyType, T13: DafnyType> Tuple14<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13> {
2143        /// Returns a borrow of the field _0
2144        pub fn _0(&self) -> &T0 {
2145            match self {
2146                Tuple14::_T14{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, } => _0,
2147            }
2148        }
2149        /// Returns a borrow of the field _1
2150        pub fn _1(&self) -> &T1 {
2151            match self {
2152                Tuple14::_T14{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, } => _1,
2153            }
2154        }
2155        /// Returns a borrow of the field _2
2156        pub fn _2(&self) -> &T2 {
2157            match self {
2158                Tuple14::_T14{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, } => _2,
2159            }
2160        }
2161        /// Returns a borrow of the field _3
2162        pub fn _3(&self) -> &T3 {
2163            match self {
2164                Tuple14::_T14{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, } => _3,
2165            }
2166        }
2167        /// Returns a borrow of the field _4
2168        pub fn _4(&self) -> &T4 {
2169            match self {
2170                Tuple14::_T14{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, } => _4,
2171            }
2172        }
2173        /// Returns a borrow of the field _5
2174        pub fn _5(&self) -> &T5 {
2175            match self {
2176                Tuple14::_T14{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, } => _5,
2177            }
2178        }
2179        /// Returns a borrow of the field _6
2180        pub fn _6(&self) -> &T6 {
2181            match self {
2182                Tuple14::_T14{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, } => _6,
2183            }
2184        }
2185        /// Returns a borrow of the field _7
2186        pub fn _7(&self) -> &T7 {
2187            match self {
2188                Tuple14::_T14{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, } => _7,
2189            }
2190        }
2191        /// Returns a borrow of the field _8
2192        pub fn _8(&self) -> &T8 {
2193            match self {
2194                Tuple14::_T14{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, } => _8,
2195            }
2196        }
2197        /// Returns a borrow of the field _9
2198        pub fn _9(&self) -> &T9 {
2199            match self {
2200                Tuple14::_T14{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, } => _9,
2201            }
2202        }
2203        /// Returns a borrow of the field _10
2204        pub fn _10(&self) -> &T10 {
2205            match self {
2206                Tuple14::_T14{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, } => _10,
2207            }
2208        }
2209        /// Returns a borrow of the field _11
2210        pub fn _11(&self) -> &T11 {
2211            match self {
2212                Tuple14::_T14{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, } => _11,
2213            }
2214        }
2215        /// Returns a borrow of the field _12
2216        pub fn _12(&self) -> &T12 {
2217            match self {
2218                Tuple14::_T14{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, } => _12,
2219            }
2220        }
2221        /// Returns a borrow of the field _13
2222        pub fn _13(&self) -> &T13 {
2223            match self {
2224                Tuple14::_T14{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, } => _13,
2225            }
2226        }
2227    }
2228
2229    impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType, T9: DafnyType, T10: DafnyType, T11: DafnyType, T12: DafnyType, T13: DafnyType> Debug
2230        for Tuple14<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13> {
2231        fn fmt(&self, f: &mut Formatter) -> Result {
2232            DafnyPrint::fmt_print(self, f, true)
2233        }
2234    }
2235
2236    impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType, T9: DafnyType, T10: DafnyType, T11: DafnyType, T12: DafnyType, T13: DafnyType> DafnyPrint
2237        for Tuple14<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13> {
2238        fn fmt_print(&self, _formatter: &mut Formatter, _in_seq: bool) -> std::fmt::Result {
2239            match self {
2240                Tuple14::_T14{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, } => {
2241                    write!(_formatter, "(")?;
2242                    DafnyPrint::fmt_print(_0, _formatter, false)?;
2243                    write!(_formatter, ", ")?;
2244                    DafnyPrint::fmt_print(_1, _formatter, false)?;
2245                    write!(_formatter, ", ")?;
2246                    DafnyPrint::fmt_print(_2, _formatter, false)?;
2247                    write!(_formatter, ", ")?;
2248                    DafnyPrint::fmt_print(_3, _formatter, false)?;
2249                    write!(_formatter, ", ")?;
2250                    DafnyPrint::fmt_print(_4, _formatter, false)?;
2251                    write!(_formatter, ", ")?;
2252                    DafnyPrint::fmt_print(_5, _formatter, false)?;
2253                    write!(_formatter, ", ")?;
2254                    DafnyPrint::fmt_print(_6, _formatter, false)?;
2255                    write!(_formatter, ", ")?;
2256                    DafnyPrint::fmt_print(_7, _formatter, false)?;
2257                    write!(_formatter, ", ")?;
2258                    DafnyPrint::fmt_print(_8, _formatter, false)?;
2259                    write!(_formatter, ", ")?;
2260                    DafnyPrint::fmt_print(_9, _formatter, false)?;
2261                    write!(_formatter, ", ")?;
2262                    DafnyPrint::fmt_print(_10, _formatter, false)?;
2263                    write!(_formatter, ", ")?;
2264                    DafnyPrint::fmt_print(_11, _formatter, false)?;
2265                    write!(_formatter, ", ")?;
2266                    DafnyPrint::fmt_print(_12, _formatter, false)?;
2267                    write!(_formatter, ", ")?;
2268                    DafnyPrint::fmt_print(_13, _formatter, false)?;
2269                    write!(_formatter, ")")?;
2270                    Ok(())
2271                },
2272            }
2273        }
2274    }
2275
2276    impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType, T9: DafnyType, T10: DafnyType, T11: DafnyType, T12: DafnyType, T13: DafnyType> Tuple14<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13> {
2277        /// Given type parameter conversions, returns a lambda to convert this structure
2278        pub fn coerce<__T0: DafnyType, __T1: DafnyType, __T2: DafnyType, __T3: DafnyType, __T4: DafnyType, __T5: DafnyType, __T6: DafnyType, __T7: DafnyType, __T8: DafnyType, __T9: DafnyType, __T10: DafnyType, __T11: DafnyType, __T12: DafnyType, __T13: DafnyType>(f_0: Rc<impl ::std::ops::Fn(T0) -> __T0 + 'static>, f_1: Rc<impl ::std::ops::Fn(T1) -> __T1 + 'static>, f_2: Rc<impl ::std::ops::Fn(T2) -> __T2 + 'static>, f_3: Rc<impl ::std::ops::Fn(T3) -> __T3 + 'static>, f_4: Rc<impl ::std::ops::Fn(T4) -> __T4 + 'static>, f_5: Rc<impl ::std::ops::Fn(T5) -> __T5 + 'static>, f_6: Rc<impl ::std::ops::Fn(T6) -> __T6 + 'static>, f_7: Rc<impl ::std::ops::Fn(T7) -> __T7 + 'static>, f_8: Rc<impl ::std::ops::Fn(T8) -> __T8 + 'static>, f_9: Rc<impl ::std::ops::Fn(T9) -> __T9 + 'static>, f_10: Rc<impl ::std::ops::Fn(T10) -> __T10 + 'static>, f_11: Rc<impl ::std::ops::Fn(T11) -> __T11 + 'static>, f_12: Rc<impl ::std::ops::Fn(T12) -> __T12 + 'static>, f_13: Rc<impl ::std::ops::Fn(T13) -> __T13 + 'static>) -> Rc<impl ::std::ops::Fn(Tuple14<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13>) -> Tuple14<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8, __T9, __T10, __T11, __T12, __T13>> {
2279            Rc::new(move |this: Self| -> Tuple14<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8, __T9, __T10, __T11, __T12, __T13>{
2280                    match this {
2281                        Tuple14::_T14{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, } => {
2282                            Tuple14::_T14 {
2283                                _0: f_0.clone()(_0),
2284                                _1: f_1.clone()(_1),
2285                                _2: f_2.clone()(_2),
2286                                _3: f_3.clone()(_3),
2287                                _4: f_4.clone()(_4),
2288                                _5: f_5.clone()(_5),
2289                                _6: f_6.clone()(_6),
2290                                _7: f_7.clone()(_7),
2291                                _8: f_8.clone()(_8),
2292                                _9: f_9.clone()(_9),
2293                                _10: f_10.clone()(_10),
2294                                _11: f_11.clone()(_11),
2295                                _12: f_12.clone()(_12),
2296                                _13: f_13.clone()(_13)
2297                            }
2298                        },
2299                    }
2300                })
2301        }
2302    }
2303
2304    impl<T0: DafnyType + Eq + Hash, T1: DafnyType + Eq + Hash, T2: DafnyType + Eq + Hash, T3: DafnyType + Eq + Hash, T4: DafnyType + Eq + Hash, T5: DafnyType + Eq + Hash, T6: DafnyType + Eq + Hash, T7: DafnyType + Eq + Hash, T8: DafnyType + Eq + Hash, T9: DafnyType + Eq + Hash, T10: DafnyType + Eq + Hash, T11: DafnyType + Eq + Hash, T12: DafnyType + Eq + Hash, T13: DafnyType + Eq + Hash> PartialEq
2305        for Tuple14<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13> {
2306        fn eq(&self, other: &Self) -> bool {
2307            match (
2308                    self,
2309                    other
2310                ) {
2311                (Tuple14::_T14{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, }, Tuple14::_T14{_0: _2__0, _1: _2__1, _2: _2__2, _3: _2__3, _4: _2__4, _5: _2__5, _6: _2__6, _7: _2__7, _8: _2__8, _9: _2__9, _10: _2__10, _11: _2__11, _12: _2__12, _13: _2__13, }) => {
2312                    _0 == _2__0 && _1 == _2__1 && _2 == _2__2 && _3 == _2__3 && _4 == _2__4 && _5 == _2__5 && _6 == _2__6 && _7 == _2__7 && _8 == _2__8 && _9 == _2__9 && _10 == _2__10 && _11 == _2__11 && _12 == _2__12 && _13 == _2__13
2313                },
2314                _ => {
2315                    false
2316                },
2317            }
2318        }
2319    }
2320
2321    impl<T0: DafnyType + Eq + Hash, T1: DafnyType + Eq + Hash, T2: DafnyType + Eq + Hash, T3: DafnyType + Eq + Hash, T4: DafnyType + Eq + Hash, T5: DafnyType + Eq + Hash, T6: DafnyType + Eq + Hash, T7: DafnyType + Eq + Hash, T8: DafnyType + Eq + Hash, T9: DafnyType + Eq + Hash, T10: DafnyType + Eq + Hash, T11: DafnyType + Eq + Hash, T12: DafnyType + Eq + Hash, T13: DafnyType + Eq + Hash> Eq
2322        for Tuple14<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13> {}
2323
2324    impl<T0: DafnyType + Hash, T1: DafnyType + Hash, T2: DafnyType + Hash, T3: DafnyType + Hash, T4: DafnyType + Hash, T5: DafnyType + Hash, T6: DafnyType + Hash, T7: DafnyType + Hash, T8: DafnyType + Hash, T9: DafnyType + Hash, T10: DafnyType + Hash, T11: DafnyType + Hash, T12: DafnyType + Hash, T13: DafnyType + Hash> Hash
2325        for Tuple14<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13> {
2326        fn hash<_H: Hasher>(&self, _state: &mut _H) {
2327            match self {
2328                Tuple14::_T14{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, } => {
2329                    Hash::hash(_0, _state);
2330                    Hash::hash(_1, _state);
2331                    Hash::hash(_2, _state);
2332                    Hash::hash(_3, _state);
2333                    Hash::hash(_4, _state);
2334                    Hash::hash(_5, _state);
2335                    Hash::hash(_6, _state);
2336                    Hash::hash(_7, _state);
2337                    Hash::hash(_8, _state);
2338                    Hash::hash(_9, _state);
2339                    Hash::hash(_10, _state);
2340                    Hash::hash(_11, _state);
2341                    Hash::hash(_12, _state);
2342                    Hash::hash(_13, _state)
2343                },
2344            }
2345        }
2346    }
2347
2348    impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType, T9: DafnyType, T10: DafnyType, T11: DafnyType, T12: DafnyType, T13: DafnyType> AsRef<Tuple14<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13>>
2349        for Tuple14<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13> {
2350        fn as_ref(&self) -> &Self {
2351            self
2352        }
2353    }
2354
2355    #[derive(Clone)]
2356    pub enum Tuple15<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType, T9: DafnyType, T10: DafnyType, T11: DafnyType, T12: DafnyType, T13: DafnyType, T14: DafnyType> {
2357        _T15 {
2358            _0: T0,
2359            _1: T1,
2360            _2: T2,
2361            _3: T3,
2362            _4: T4,
2363            _5: T5,
2364            _6: T6,
2365            _7: T7,
2366            _8: T8,
2367            _9: T9,
2368            _10: T10,
2369            _11: T11,
2370            _12: T12,
2371            _13: T13,
2372            _14: T14
2373        }
2374    }
2375
2376    impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType, T9: DafnyType, T10: DafnyType, T11: DafnyType, T12: DafnyType, T13: DafnyType, T14: DafnyType> Tuple15<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14> {
2377        /// Returns a borrow of the field _0
2378        pub fn _0(&self) -> &T0 {
2379            match self {
2380                Tuple15::_T15{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, } => _0,
2381            }
2382        }
2383        /// Returns a borrow of the field _1
2384        pub fn _1(&self) -> &T1 {
2385            match self {
2386                Tuple15::_T15{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, } => _1,
2387            }
2388        }
2389        /// Returns a borrow of the field _2
2390        pub fn _2(&self) -> &T2 {
2391            match self {
2392                Tuple15::_T15{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, } => _2,
2393            }
2394        }
2395        /// Returns a borrow of the field _3
2396        pub fn _3(&self) -> &T3 {
2397            match self {
2398                Tuple15::_T15{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, } => _3,
2399            }
2400        }
2401        /// Returns a borrow of the field _4
2402        pub fn _4(&self) -> &T4 {
2403            match self {
2404                Tuple15::_T15{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, } => _4,
2405            }
2406        }
2407        /// Returns a borrow of the field _5
2408        pub fn _5(&self) -> &T5 {
2409            match self {
2410                Tuple15::_T15{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, } => _5,
2411            }
2412        }
2413        /// Returns a borrow of the field _6
2414        pub fn _6(&self) -> &T6 {
2415            match self {
2416                Tuple15::_T15{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, } => _6,
2417            }
2418        }
2419        /// Returns a borrow of the field _7
2420        pub fn _7(&self) -> &T7 {
2421            match self {
2422                Tuple15::_T15{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, } => _7,
2423            }
2424        }
2425        /// Returns a borrow of the field _8
2426        pub fn _8(&self) -> &T8 {
2427            match self {
2428                Tuple15::_T15{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, } => _8,
2429            }
2430        }
2431        /// Returns a borrow of the field _9
2432        pub fn _9(&self) -> &T9 {
2433            match self {
2434                Tuple15::_T15{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, } => _9,
2435            }
2436        }
2437        /// Returns a borrow of the field _10
2438        pub fn _10(&self) -> &T10 {
2439            match self {
2440                Tuple15::_T15{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, } => _10,
2441            }
2442        }
2443        /// Returns a borrow of the field _11
2444        pub fn _11(&self) -> &T11 {
2445            match self {
2446                Tuple15::_T15{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, } => _11,
2447            }
2448        }
2449        /// Returns a borrow of the field _12
2450        pub fn _12(&self) -> &T12 {
2451            match self {
2452                Tuple15::_T15{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, } => _12,
2453            }
2454        }
2455        /// Returns a borrow of the field _13
2456        pub fn _13(&self) -> &T13 {
2457            match self {
2458                Tuple15::_T15{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, } => _13,
2459            }
2460        }
2461        /// Returns a borrow of the field _14
2462        pub fn _14(&self) -> &T14 {
2463            match self {
2464                Tuple15::_T15{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, } => _14,
2465            }
2466        }
2467    }
2468
2469    impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType, T9: DafnyType, T10: DafnyType, T11: DafnyType, T12: DafnyType, T13: DafnyType, T14: DafnyType> Debug
2470        for Tuple15<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14> {
2471        fn fmt(&self, f: &mut Formatter) -> Result {
2472            DafnyPrint::fmt_print(self, f, true)
2473        }
2474    }
2475
2476    impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType, T9: DafnyType, T10: DafnyType, T11: DafnyType, T12: DafnyType, T13: DafnyType, T14: DafnyType> DafnyPrint
2477        for Tuple15<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14> {
2478        fn fmt_print(&self, _formatter: &mut Formatter, _in_seq: bool) -> std::fmt::Result {
2479            match self {
2480                Tuple15::_T15{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, } => {
2481                    write!(_formatter, "(")?;
2482                    DafnyPrint::fmt_print(_0, _formatter, false)?;
2483                    write!(_formatter, ", ")?;
2484                    DafnyPrint::fmt_print(_1, _formatter, false)?;
2485                    write!(_formatter, ", ")?;
2486                    DafnyPrint::fmt_print(_2, _formatter, false)?;
2487                    write!(_formatter, ", ")?;
2488                    DafnyPrint::fmt_print(_3, _formatter, false)?;
2489                    write!(_formatter, ", ")?;
2490                    DafnyPrint::fmt_print(_4, _formatter, false)?;
2491                    write!(_formatter, ", ")?;
2492                    DafnyPrint::fmt_print(_5, _formatter, false)?;
2493                    write!(_formatter, ", ")?;
2494                    DafnyPrint::fmt_print(_6, _formatter, false)?;
2495                    write!(_formatter, ", ")?;
2496                    DafnyPrint::fmt_print(_7, _formatter, false)?;
2497                    write!(_formatter, ", ")?;
2498                    DafnyPrint::fmt_print(_8, _formatter, false)?;
2499                    write!(_formatter, ", ")?;
2500                    DafnyPrint::fmt_print(_9, _formatter, false)?;
2501                    write!(_formatter, ", ")?;
2502                    DafnyPrint::fmt_print(_10, _formatter, false)?;
2503                    write!(_formatter, ", ")?;
2504                    DafnyPrint::fmt_print(_11, _formatter, false)?;
2505                    write!(_formatter, ", ")?;
2506                    DafnyPrint::fmt_print(_12, _formatter, false)?;
2507                    write!(_formatter, ", ")?;
2508                    DafnyPrint::fmt_print(_13, _formatter, false)?;
2509                    write!(_formatter, ", ")?;
2510                    DafnyPrint::fmt_print(_14, _formatter, false)?;
2511                    write!(_formatter, ")")?;
2512                    Ok(())
2513                },
2514            }
2515        }
2516    }
2517
2518    impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType, T9: DafnyType, T10: DafnyType, T11: DafnyType, T12: DafnyType, T13: DafnyType, T14: DafnyType> Tuple15<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14> {
2519        /// Given type parameter conversions, returns a lambda to convert this structure
2520        pub fn coerce<__T0: DafnyType, __T1: DafnyType, __T2: DafnyType, __T3: DafnyType, __T4: DafnyType, __T5: DafnyType, __T6: DafnyType, __T7: DafnyType, __T8: DafnyType, __T9: DafnyType, __T10: DafnyType, __T11: DafnyType, __T12: DafnyType, __T13: DafnyType, __T14: DafnyType>(f_0: Rc<impl ::std::ops::Fn(T0) -> __T0 + 'static>, f_1: Rc<impl ::std::ops::Fn(T1) -> __T1 + 'static>, f_2: Rc<impl ::std::ops::Fn(T2) -> __T2 + 'static>, f_3: Rc<impl ::std::ops::Fn(T3) -> __T3 + 'static>, f_4: Rc<impl ::std::ops::Fn(T4) -> __T4 + 'static>, f_5: Rc<impl ::std::ops::Fn(T5) -> __T5 + 'static>, f_6: Rc<impl ::std::ops::Fn(T6) -> __T6 + 'static>, f_7: Rc<impl ::std::ops::Fn(T7) -> __T7 + 'static>, f_8: Rc<impl ::std::ops::Fn(T8) -> __T8 + 'static>, f_9: Rc<impl ::std::ops::Fn(T9) -> __T9 + 'static>, f_10: Rc<impl ::std::ops::Fn(T10) -> __T10 + 'static>, f_11: Rc<impl ::std::ops::Fn(T11) -> __T11 + 'static>, f_12: Rc<impl ::std::ops::Fn(T12) -> __T12 + 'static>, f_13: Rc<impl ::std::ops::Fn(T13) -> __T13 + 'static>, f_14: Rc<impl ::std::ops::Fn(T14) -> __T14 + 'static>) -> Rc<impl ::std::ops::Fn(Tuple15<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14>) -> Tuple15<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8, __T9, __T10, __T11, __T12, __T13, __T14>> {
2521            Rc::new(move |this: Self| -> Tuple15<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8, __T9, __T10, __T11, __T12, __T13, __T14>{
2522                    match this {
2523                        Tuple15::_T15{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, } => {
2524                            Tuple15::_T15 {
2525                                _0: f_0.clone()(_0),
2526                                _1: f_1.clone()(_1),
2527                                _2: f_2.clone()(_2),
2528                                _3: f_3.clone()(_3),
2529                                _4: f_4.clone()(_4),
2530                                _5: f_5.clone()(_5),
2531                                _6: f_6.clone()(_6),
2532                                _7: f_7.clone()(_7),
2533                                _8: f_8.clone()(_8),
2534                                _9: f_9.clone()(_9),
2535                                _10: f_10.clone()(_10),
2536                                _11: f_11.clone()(_11),
2537                                _12: f_12.clone()(_12),
2538                                _13: f_13.clone()(_13),
2539                                _14: f_14.clone()(_14)
2540                            }
2541                        },
2542                    }
2543                })
2544        }
2545    }
2546
2547    impl<T0: DafnyType + Eq + Hash, T1: DafnyType + Eq + Hash, T2: DafnyType + Eq + Hash, T3: DafnyType + Eq + Hash, T4: DafnyType + Eq + Hash, T5: DafnyType + Eq + Hash, T6: DafnyType + Eq + Hash, T7: DafnyType + Eq + Hash, T8: DafnyType + Eq + Hash, T9: DafnyType + Eq + Hash, T10: DafnyType + Eq + Hash, T11: DafnyType + Eq + Hash, T12: DafnyType + Eq + Hash, T13: DafnyType + Eq + Hash, T14: DafnyType + Eq + Hash> PartialEq
2548        for Tuple15<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14> {
2549        fn eq(&self, other: &Self) -> bool {
2550            match (
2551                    self,
2552                    other
2553                ) {
2554                (Tuple15::_T15{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, }, Tuple15::_T15{_0: _2__0, _1: _2__1, _2: _2__2, _3: _2__3, _4: _2__4, _5: _2__5, _6: _2__6, _7: _2__7, _8: _2__8, _9: _2__9, _10: _2__10, _11: _2__11, _12: _2__12, _13: _2__13, _14: _2__14, }) => {
2555                    _0 == _2__0 && _1 == _2__1 && _2 == _2__2 && _3 == _2__3 && _4 == _2__4 && _5 == _2__5 && _6 == _2__6 && _7 == _2__7 && _8 == _2__8 && _9 == _2__9 && _10 == _2__10 && _11 == _2__11 && _12 == _2__12 && _13 == _2__13 && _14 == _2__14
2556                },
2557                _ => {
2558                    false
2559                },
2560            }
2561        }
2562    }
2563
2564    impl<T0: DafnyType + Eq + Hash, T1: DafnyType + Eq + Hash, T2: DafnyType + Eq + Hash, T3: DafnyType + Eq + Hash, T4: DafnyType + Eq + Hash, T5: DafnyType + Eq + Hash, T6: DafnyType + Eq + Hash, T7: DafnyType + Eq + Hash, T8: DafnyType + Eq + Hash, T9: DafnyType + Eq + Hash, T10: DafnyType + Eq + Hash, T11: DafnyType + Eq + Hash, T12: DafnyType + Eq + Hash, T13: DafnyType + Eq + Hash, T14: DafnyType + Eq + Hash> Eq
2565        for Tuple15<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14> {}
2566
2567    impl<T0: DafnyType + Hash, T1: DafnyType + Hash, T2: DafnyType + Hash, T3: DafnyType + Hash, T4: DafnyType + Hash, T5: DafnyType + Hash, T6: DafnyType + Hash, T7: DafnyType + Hash, T8: DafnyType + Hash, T9: DafnyType + Hash, T10: DafnyType + Hash, T11: DafnyType + Hash, T12: DafnyType + Hash, T13: DafnyType + Hash, T14: DafnyType + Hash> Hash
2568        for Tuple15<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14> {
2569        fn hash<_H: Hasher>(&self, _state: &mut _H) {
2570            match self {
2571                Tuple15::_T15{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, } => {
2572                    Hash::hash(_0, _state);
2573                    Hash::hash(_1, _state);
2574                    Hash::hash(_2, _state);
2575                    Hash::hash(_3, _state);
2576                    Hash::hash(_4, _state);
2577                    Hash::hash(_5, _state);
2578                    Hash::hash(_6, _state);
2579                    Hash::hash(_7, _state);
2580                    Hash::hash(_8, _state);
2581                    Hash::hash(_9, _state);
2582                    Hash::hash(_10, _state);
2583                    Hash::hash(_11, _state);
2584                    Hash::hash(_12, _state);
2585                    Hash::hash(_13, _state);
2586                    Hash::hash(_14, _state)
2587                },
2588            }
2589        }
2590    }
2591
2592    impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType, T9: DafnyType, T10: DafnyType, T11: DafnyType, T12: DafnyType, T13: DafnyType, T14: DafnyType> AsRef<Tuple15<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14>>
2593        for Tuple15<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14> {
2594        fn as_ref(&self) -> &Self {
2595            self
2596        }
2597    }
2598
2599    #[derive(Clone)]
2600    pub enum Tuple16<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType, T9: DafnyType, T10: DafnyType, T11: DafnyType, T12: DafnyType, T13: DafnyType, T14: DafnyType, T15: DafnyType> {
2601        _T16 {
2602            _0: T0,
2603            _1: T1,
2604            _2: T2,
2605            _3: T3,
2606            _4: T4,
2607            _5: T5,
2608            _6: T6,
2609            _7: T7,
2610            _8: T8,
2611            _9: T9,
2612            _10: T10,
2613            _11: T11,
2614            _12: T12,
2615            _13: T13,
2616            _14: T14,
2617            _15: T15
2618        }
2619    }
2620
2621    impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType, T9: DafnyType, T10: DafnyType, T11: DafnyType, T12: DafnyType, T13: DafnyType, T14: DafnyType, T15: DafnyType> Tuple16<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15> {
2622        /// Returns a borrow of the field _0
2623        pub fn _0(&self) -> &T0 {
2624            match self {
2625                Tuple16::_T16{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, } => _0,
2626            }
2627        }
2628        /// Returns a borrow of the field _1
2629        pub fn _1(&self) -> &T1 {
2630            match self {
2631                Tuple16::_T16{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, } => _1,
2632            }
2633        }
2634        /// Returns a borrow of the field _2
2635        pub fn _2(&self) -> &T2 {
2636            match self {
2637                Tuple16::_T16{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, } => _2,
2638            }
2639        }
2640        /// Returns a borrow of the field _3
2641        pub fn _3(&self) -> &T3 {
2642            match self {
2643                Tuple16::_T16{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, } => _3,
2644            }
2645        }
2646        /// Returns a borrow of the field _4
2647        pub fn _4(&self) -> &T4 {
2648            match self {
2649                Tuple16::_T16{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, } => _4,
2650            }
2651        }
2652        /// Returns a borrow of the field _5
2653        pub fn _5(&self) -> &T5 {
2654            match self {
2655                Tuple16::_T16{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, } => _5,
2656            }
2657        }
2658        /// Returns a borrow of the field _6
2659        pub fn _6(&self) -> &T6 {
2660            match self {
2661                Tuple16::_T16{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, } => _6,
2662            }
2663        }
2664        /// Returns a borrow of the field _7
2665        pub fn _7(&self) -> &T7 {
2666            match self {
2667                Tuple16::_T16{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, } => _7,
2668            }
2669        }
2670        /// Returns a borrow of the field _8
2671        pub fn _8(&self) -> &T8 {
2672            match self {
2673                Tuple16::_T16{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, } => _8,
2674            }
2675        }
2676        /// Returns a borrow of the field _9
2677        pub fn _9(&self) -> &T9 {
2678            match self {
2679                Tuple16::_T16{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, } => _9,
2680            }
2681        }
2682        /// Returns a borrow of the field _10
2683        pub fn _10(&self) -> &T10 {
2684            match self {
2685                Tuple16::_T16{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, } => _10,
2686            }
2687        }
2688        /// Returns a borrow of the field _11
2689        pub fn _11(&self) -> &T11 {
2690            match self {
2691                Tuple16::_T16{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, } => _11,
2692            }
2693        }
2694        /// Returns a borrow of the field _12
2695        pub fn _12(&self) -> &T12 {
2696            match self {
2697                Tuple16::_T16{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, } => _12,
2698            }
2699        }
2700        /// Returns a borrow of the field _13
2701        pub fn _13(&self) -> &T13 {
2702            match self {
2703                Tuple16::_T16{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, } => _13,
2704            }
2705        }
2706        /// Returns a borrow of the field _14
2707        pub fn _14(&self) -> &T14 {
2708            match self {
2709                Tuple16::_T16{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, } => _14,
2710            }
2711        }
2712        /// Returns a borrow of the field _15
2713        pub fn _15(&self) -> &T15 {
2714            match self {
2715                Tuple16::_T16{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, } => _15,
2716            }
2717        }
2718    }
2719
2720    impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType, T9: DafnyType, T10: DafnyType, T11: DafnyType, T12: DafnyType, T13: DafnyType, T14: DafnyType, T15: DafnyType> Debug
2721        for Tuple16<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15> {
2722        fn fmt(&self, f: &mut Formatter) -> Result {
2723            DafnyPrint::fmt_print(self, f, true)
2724        }
2725    }
2726
2727    impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType, T9: DafnyType, T10: DafnyType, T11: DafnyType, T12: DafnyType, T13: DafnyType, T14: DafnyType, T15: DafnyType> DafnyPrint
2728        for Tuple16<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15> {
2729        fn fmt_print(&self, _formatter: &mut Formatter, _in_seq: bool) -> std::fmt::Result {
2730            match self {
2731                Tuple16::_T16{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, } => {
2732                    write!(_formatter, "(")?;
2733                    DafnyPrint::fmt_print(_0, _formatter, false)?;
2734                    write!(_formatter, ", ")?;
2735                    DafnyPrint::fmt_print(_1, _formatter, false)?;
2736                    write!(_formatter, ", ")?;
2737                    DafnyPrint::fmt_print(_2, _formatter, false)?;
2738                    write!(_formatter, ", ")?;
2739                    DafnyPrint::fmt_print(_3, _formatter, false)?;
2740                    write!(_formatter, ", ")?;
2741                    DafnyPrint::fmt_print(_4, _formatter, false)?;
2742                    write!(_formatter, ", ")?;
2743                    DafnyPrint::fmt_print(_5, _formatter, false)?;
2744                    write!(_formatter, ", ")?;
2745                    DafnyPrint::fmt_print(_6, _formatter, false)?;
2746                    write!(_formatter, ", ")?;
2747                    DafnyPrint::fmt_print(_7, _formatter, false)?;
2748                    write!(_formatter, ", ")?;
2749                    DafnyPrint::fmt_print(_8, _formatter, false)?;
2750                    write!(_formatter, ", ")?;
2751                    DafnyPrint::fmt_print(_9, _formatter, false)?;
2752                    write!(_formatter, ", ")?;
2753                    DafnyPrint::fmt_print(_10, _formatter, false)?;
2754                    write!(_formatter, ", ")?;
2755                    DafnyPrint::fmt_print(_11, _formatter, false)?;
2756                    write!(_formatter, ", ")?;
2757                    DafnyPrint::fmt_print(_12, _formatter, false)?;
2758                    write!(_formatter, ", ")?;
2759                    DafnyPrint::fmt_print(_13, _formatter, false)?;
2760                    write!(_formatter, ", ")?;
2761                    DafnyPrint::fmt_print(_14, _formatter, false)?;
2762                    write!(_formatter, ", ")?;
2763                    DafnyPrint::fmt_print(_15, _formatter, false)?;
2764                    write!(_formatter, ")")?;
2765                    Ok(())
2766                },
2767            }
2768        }
2769    }
2770
2771    impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType, T9: DafnyType, T10: DafnyType, T11: DafnyType, T12: DafnyType, T13: DafnyType, T14: DafnyType, T15: DafnyType> Tuple16<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15> {
2772        /// Given type parameter conversions, returns a lambda to convert this structure
2773        pub fn coerce<__T0: DafnyType, __T1: DafnyType, __T2: DafnyType, __T3: DafnyType, __T4: DafnyType, __T5: DafnyType, __T6: DafnyType, __T7: DafnyType, __T8: DafnyType, __T9: DafnyType, __T10: DafnyType, __T11: DafnyType, __T12: DafnyType, __T13: DafnyType, __T14: DafnyType, __T15: DafnyType>(f_0: Rc<impl ::std::ops::Fn(T0) -> __T0 + 'static>, f_1: Rc<impl ::std::ops::Fn(T1) -> __T1 + 'static>, f_2: Rc<impl ::std::ops::Fn(T2) -> __T2 + 'static>, f_3: Rc<impl ::std::ops::Fn(T3) -> __T3 + 'static>, f_4: Rc<impl ::std::ops::Fn(T4) -> __T4 + 'static>, f_5: Rc<impl ::std::ops::Fn(T5) -> __T5 + 'static>, f_6: Rc<impl ::std::ops::Fn(T6) -> __T6 + 'static>, f_7: Rc<impl ::std::ops::Fn(T7) -> __T7 + 'static>, f_8: Rc<impl ::std::ops::Fn(T8) -> __T8 + 'static>, f_9: Rc<impl ::std::ops::Fn(T9) -> __T9 + 'static>, f_10: Rc<impl ::std::ops::Fn(T10) -> __T10 + 'static>, f_11: Rc<impl ::std::ops::Fn(T11) -> __T11 + 'static>, f_12: Rc<impl ::std::ops::Fn(T12) -> __T12 + 'static>, f_13: Rc<impl ::std::ops::Fn(T13) -> __T13 + 'static>, f_14: Rc<impl ::std::ops::Fn(T14) -> __T14 + 'static>, f_15: Rc<impl ::std::ops::Fn(T15) -> __T15 + 'static>) -> Rc<impl ::std::ops::Fn(Tuple16<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15>) -> Tuple16<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8, __T9, __T10, __T11, __T12, __T13, __T14, __T15>> {
2774            Rc::new(move |this: Self| -> Tuple16<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8, __T9, __T10, __T11, __T12, __T13, __T14, __T15>{
2775                    match this {
2776                        Tuple16::_T16{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, } => {
2777                            Tuple16::_T16 {
2778                                _0: f_0.clone()(_0),
2779                                _1: f_1.clone()(_1),
2780                                _2: f_2.clone()(_2),
2781                                _3: f_3.clone()(_3),
2782                                _4: f_4.clone()(_4),
2783                                _5: f_5.clone()(_5),
2784                                _6: f_6.clone()(_6),
2785                                _7: f_7.clone()(_7),
2786                                _8: f_8.clone()(_8),
2787                                _9: f_9.clone()(_9),
2788                                _10: f_10.clone()(_10),
2789                                _11: f_11.clone()(_11),
2790                                _12: f_12.clone()(_12),
2791                                _13: f_13.clone()(_13),
2792                                _14: f_14.clone()(_14),
2793                                _15: f_15.clone()(_15)
2794                            }
2795                        },
2796                    }
2797                })
2798        }
2799    }
2800
2801    impl<T0: DafnyType + Eq + Hash, T1: DafnyType + Eq + Hash, T2: DafnyType + Eq + Hash, T3: DafnyType + Eq + Hash, T4: DafnyType + Eq + Hash, T5: DafnyType + Eq + Hash, T6: DafnyType + Eq + Hash, T7: DafnyType + Eq + Hash, T8: DafnyType + Eq + Hash, T9: DafnyType + Eq + Hash, T10: DafnyType + Eq + Hash, T11: DafnyType + Eq + Hash, T12: DafnyType + Eq + Hash, T13: DafnyType + Eq + Hash, T14: DafnyType + Eq + Hash, T15: DafnyType + Eq + Hash> PartialEq
2802        for Tuple16<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15> {
2803        fn eq(&self, other: &Self) -> bool {
2804            match (
2805                    self,
2806                    other
2807                ) {
2808                (Tuple16::_T16{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, }, Tuple16::_T16{_0: _2__0, _1: _2__1, _2: _2__2, _3: _2__3, _4: _2__4, _5: _2__5, _6: _2__6, _7: _2__7, _8: _2__8, _9: _2__9, _10: _2__10, _11: _2__11, _12: _2__12, _13: _2__13, _14: _2__14, _15: _2__15, }) => {
2809                    _0 == _2__0 && _1 == _2__1 && _2 == _2__2 && _3 == _2__3 && _4 == _2__4 && _5 == _2__5 && _6 == _2__6 && _7 == _2__7 && _8 == _2__8 && _9 == _2__9 && _10 == _2__10 && _11 == _2__11 && _12 == _2__12 && _13 == _2__13 && _14 == _2__14 && _15 == _2__15
2810                },
2811                _ => {
2812                    false
2813                },
2814            }
2815        }
2816    }
2817
2818    impl<T0: DafnyType + Eq + Hash, T1: DafnyType + Eq + Hash, T2: DafnyType + Eq + Hash, T3: DafnyType + Eq + Hash, T4: DafnyType + Eq + Hash, T5: DafnyType + Eq + Hash, T6: DafnyType + Eq + Hash, T7: DafnyType + Eq + Hash, T8: DafnyType + Eq + Hash, T9: DafnyType + Eq + Hash, T10: DafnyType + Eq + Hash, T11: DafnyType + Eq + Hash, T12: DafnyType + Eq + Hash, T13: DafnyType + Eq + Hash, T14: DafnyType + Eq + Hash, T15: DafnyType + Eq + Hash> Eq
2819        for Tuple16<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15> {}
2820
2821    impl<T0: DafnyType + Hash, T1: DafnyType + Hash, T2: DafnyType + Hash, T3: DafnyType + Hash, T4: DafnyType + Hash, T5: DafnyType + Hash, T6: DafnyType + Hash, T7: DafnyType + Hash, T8: DafnyType + Hash, T9: DafnyType + Hash, T10: DafnyType + Hash, T11: DafnyType + Hash, T12: DafnyType + Hash, T13: DafnyType + Hash, T14: DafnyType + Hash, T15: DafnyType + Hash> Hash
2822        for Tuple16<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15> {
2823        fn hash<_H: Hasher>(&self, _state: &mut _H) {
2824            match self {
2825                Tuple16::_T16{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, } => {
2826                    Hash::hash(_0, _state);
2827                    Hash::hash(_1, _state);
2828                    Hash::hash(_2, _state);
2829                    Hash::hash(_3, _state);
2830                    Hash::hash(_4, _state);
2831                    Hash::hash(_5, _state);
2832                    Hash::hash(_6, _state);
2833                    Hash::hash(_7, _state);
2834                    Hash::hash(_8, _state);
2835                    Hash::hash(_9, _state);
2836                    Hash::hash(_10, _state);
2837                    Hash::hash(_11, _state);
2838                    Hash::hash(_12, _state);
2839                    Hash::hash(_13, _state);
2840                    Hash::hash(_14, _state);
2841                    Hash::hash(_15, _state)
2842                },
2843            }
2844        }
2845    }
2846
2847    impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType, T9: DafnyType, T10: DafnyType, T11: DafnyType, T12: DafnyType, T13: DafnyType, T14: DafnyType, T15: DafnyType> AsRef<Tuple16<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15>>
2848        for Tuple16<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15> {
2849        fn as_ref(&self) -> &Self {
2850            self
2851        }
2852    }
2853
2854    #[derive(Clone)]
2855    pub enum Tuple17<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType, T9: DafnyType, T10: DafnyType, T11: DafnyType, T12: DafnyType, T13: DafnyType, T14: DafnyType, T15: DafnyType, T16: DafnyType> {
2856        _T17 {
2857            _0: T0,
2858            _1: T1,
2859            _2: T2,
2860            _3: T3,
2861            _4: T4,
2862            _5: T5,
2863            _6: T6,
2864            _7: T7,
2865            _8: T8,
2866            _9: T9,
2867            _10: T10,
2868            _11: T11,
2869            _12: T12,
2870            _13: T13,
2871            _14: T14,
2872            _15: T15,
2873            _16: T16
2874        }
2875    }
2876
2877    impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType, T9: DafnyType, T10: DafnyType, T11: DafnyType, T12: DafnyType, T13: DafnyType, T14: DafnyType, T15: DafnyType, T16: DafnyType> Tuple17<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15, T16> {
2878        /// Returns a borrow of the field _0
2879        pub fn _0(&self) -> &T0 {
2880            match self {
2881                Tuple17::_T17{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, } => _0,
2882            }
2883        }
2884        /// Returns a borrow of the field _1
2885        pub fn _1(&self) -> &T1 {
2886            match self {
2887                Tuple17::_T17{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, } => _1,
2888            }
2889        }
2890        /// Returns a borrow of the field _2
2891        pub fn _2(&self) -> &T2 {
2892            match self {
2893                Tuple17::_T17{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, } => _2,
2894            }
2895        }
2896        /// Returns a borrow of the field _3
2897        pub fn _3(&self) -> &T3 {
2898            match self {
2899                Tuple17::_T17{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, } => _3,
2900            }
2901        }
2902        /// Returns a borrow of the field _4
2903        pub fn _4(&self) -> &T4 {
2904            match self {
2905                Tuple17::_T17{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, } => _4,
2906            }
2907        }
2908        /// Returns a borrow of the field _5
2909        pub fn _5(&self) -> &T5 {
2910            match self {
2911                Tuple17::_T17{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, } => _5,
2912            }
2913        }
2914        /// Returns a borrow of the field _6
2915        pub fn _6(&self) -> &T6 {
2916            match self {
2917                Tuple17::_T17{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, } => _6,
2918            }
2919        }
2920        /// Returns a borrow of the field _7
2921        pub fn _7(&self) -> &T7 {
2922            match self {
2923                Tuple17::_T17{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, } => _7,
2924            }
2925        }
2926        /// Returns a borrow of the field _8
2927        pub fn _8(&self) -> &T8 {
2928            match self {
2929                Tuple17::_T17{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, } => _8,
2930            }
2931        }
2932        /// Returns a borrow of the field _9
2933        pub fn _9(&self) -> &T9 {
2934            match self {
2935                Tuple17::_T17{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, } => _9,
2936            }
2937        }
2938        /// Returns a borrow of the field _10
2939        pub fn _10(&self) -> &T10 {
2940            match self {
2941                Tuple17::_T17{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, } => _10,
2942            }
2943        }
2944        /// Returns a borrow of the field _11
2945        pub fn _11(&self) -> &T11 {
2946            match self {
2947                Tuple17::_T17{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, } => _11,
2948            }
2949        }
2950        /// Returns a borrow of the field _12
2951        pub fn _12(&self) -> &T12 {
2952            match self {
2953                Tuple17::_T17{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, } => _12,
2954            }
2955        }
2956        /// Returns a borrow of the field _13
2957        pub fn _13(&self) -> &T13 {
2958            match self {
2959                Tuple17::_T17{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, } => _13,
2960            }
2961        }
2962        /// Returns a borrow of the field _14
2963        pub fn _14(&self) -> &T14 {
2964            match self {
2965                Tuple17::_T17{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, } => _14,
2966            }
2967        }
2968        /// Returns a borrow of the field _15
2969        pub fn _15(&self) -> &T15 {
2970            match self {
2971                Tuple17::_T17{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, } => _15,
2972            }
2973        }
2974        /// Returns a borrow of the field _16
2975        pub fn _16(&self) -> &T16 {
2976            match self {
2977                Tuple17::_T17{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, } => _16,
2978            }
2979        }
2980    }
2981
2982    impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType, T9: DafnyType, T10: DafnyType, T11: DafnyType, T12: DafnyType, T13: DafnyType, T14: DafnyType, T15: DafnyType, T16: DafnyType> Debug
2983        for Tuple17<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15, T16> {
2984        fn fmt(&self, f: &mut Formatter) -> Result {
2985            DafnyPrint::fmt_print(self, f, true)
2986        }
2987    }
2988
2989    impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType, T9: DafnyType, T10: DafnyType, T11: DafnyType, T12: DafnyType, T13: DafnyType, T14: DafnyType, T15: DafnyType, T16: DafnyType> DafnyPrint
2990        for Tuple17<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15, T16> {
2991        fn fmt_print(&self, _formatter: &mut Formatter, _in_seq: bool) -> std::fmt::Result {
2992            match self {
2993                Tuple17::_T17{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, } => {
2994                    write!(_formatter, "(")?;
2995                    DafnyPrint::fmt_print(_0, _formatter, false)?;
2996                    write!(_formatter, ", ")?;
2997                    DafnyPrint::fmt_print(_1, _formatter, false)?;
2998                    write!(_formatter, ", ")?;
2999                    DafnyPrint::fmt_print(_2, _formatter, false)?;
3000                    write!(_formatter, ", ")?;
3001                    DafnyPrint::fmt_print(_3, _formatter, false)?;
3002                    write!(_formatter, ", ")?;
3003                    DafnyPrint::fmt_print(_4, _formatter, false)?;
3004                    write!(_formatter, ", ")?;
3005                    DafnyPrint::fmt_print(_5, _formatter, false)?;
3006                    write!(_formatter, ", ")?;
3007                    DafnyPrint::fmt_print(_6, _formatter, false)?;
3008                    write!(_formatter, ", ")?;
3009                    DafnyPrint::fmt_print(_7, _formatter, false)?;
3010                    write!(_formatter, ", ")?;
3011                    DafnyPrint::fmt_print(_8, _formatter, false)?;
3012                    write!(_formatter, ", ")?;
3013                    DafnyPrint::fmt_print(_9, _formatter, false)?;
3014                    write!(_formatter, ", ")?;
3015                    DafnyPrint::fmt_print(_10, _formatter, false)?;
3016                    write!(_formatter, ", ")?;
3017                    DafnyPrint::fmt_print(_11, _formatter, false)?;
3018                    write!(_formatter, ", ")?;
3019                    DafnyPrint::fmt_print(_12, _formatter, false)?;
3020                    write!(_formatter, ", ")?;
3021                    DafnyPrint::fmt_print(_13, _formatter, false)?;
3022                    write!(_formatter, ", ")?;
3023                    DafnyPrint::fmt_print(_14, _formatter, false)?;
3024                    write!(_formatter, ", ")?;
3025                    DafnyPrint::fmt_print(_15, _formatter, false)?;
3026                    write!(_formatter, ", ")?;
3027                    DafnyPrint::fmt_print(_16, _formatter, false)?;
3028                    write!(_formatter, ")")?;
3029                    Ok(())
3030                },
3031            }
3032        }
3033    }
3034
3035    impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType, T9: DafnyType, T10: DafnyType, T11: DafnyType, T12: DafnyType, T13: DafnyType, T14: DafnyType, T15: DafnyType, T16: DafnyType> Tuple17<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15, T16> {
3036        /// Given type parameter conversions, returns a lambda to convert this structure
3037        pub fn coerce<__T0: DafnyType, __T1: DafnyType, __T2: DafnyType, __T3: DafnyType, __T4: DafnyType, __T5: DafnyType, __T6: DafnyType, __T7: DafnyType, __T8: DafnyType, __T9: DafnyType, __T10: DafnyType, __T11: DafnyType, __T12: DafnyType, __T13: DafnyType, __T14: DafnyType, __T15: DafnyType, __T16: DafnyType>(f_0: Rc<impl ::std::ops::Fn(T0) -> __T0 + 'static>, f_1: Rc<impl ::std::ops::Fn(T1) -> __T1 + 'static>, f_2: Rc<impl ::std::ops::Fn(T2) -> __T2 + 'static>, f_3: Rc<impl ::std::ops::Fn(T3) -> __T3 + 'static>, f_4: Rc<impl ::std::ops::Fn(T4) -> __T4 + 'static>, f_5: Rc<impl ::std::ops::Fn(T5) -> __T5 + 'static>, f_6: Rc<impl ::std::ops::Fn(T6) -> __T6 + 'static>, f_7: Rc<impl ::std::ops::Fn(T7) -> __T7 + 'static>, f_8: Rc<impl ::std::ops::Fn(T8) -> __T8 + 'static>, f_9: Rc<impl ::std::ops::Fn(T9) -> __T9 + 'static>, f_10: Rc<impl ::std::ops::Fn(T10) -> __T10 + 'static>, f_11: Rc<impl ::std::ops::Fn(T11) -> __T11 + 'static>, f_12: Rc<impl ::std::ops::Fn(T12) -> __T12 + 'static>, f_13: Rc<impl ::std::ops::Fn(T13) -> __T13 + 'static>, f_14: Rc<impl ::std::ops::Fn(T14) -> __T14 + 'static>, f_15: Rc<impl ::std::ops::Fn(T15) -> __T15 + 'static>, f_16: Rc<impl ::std::ops::Fn(T16) -> __T16 + 'static>) -> Rc<impl ::std::ops::Fn(Tuple17<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15, T16>) -> Tuple17<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8, __T9, __T10, __T11, __T12, __T13, __T14, __T15, __T16>> {
3038            Rc::new(move |this: Self| -> Tuple17<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8, __T9, __T10, __T11, __T12, __T13, __T14, __T15, __T16>{
3039                    match this {
3040                        Tuple17::_T17{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, } => {
3041                            Tuple17::_T17 {
3042                                _0: f_0.clone()(_0),
3043                                _1: f_1.clone()(_1),
3044                                _2: f_2.clone()(_2),
3045                                _3: f_3.clone()(_3),
3046                                _4: f_4.clone()(_4),
3047                                _5: f_5.clone()(_5),
3048                                _6: f_6.clone()(_6),
3049                                _7: f_7.clone()(_7),
3050                                _8: f_8.clone()(_8),
3051                                _9: f_9.clone()(_9),
3052                                _10: f_10.clone()(_10),
3053                                _11: f_11.clone()(_11),
3054                                _12: f_12.clone()(_12),
3055                                _13: f_13.clone()(_13),
3056                                _14: f_14.clone()(_14),
3057                                _15: f_15.clone()(_15),
3058                                _16: f_16.clone()(_16)
3059                            }
3060                        },
3061                    }
3062                })
3063        }
3064    }
3065
3066    impl<T0: DafnyType + Eq + Hash, T1: DafnyType + Eq + Hash, T2: DafnyType + Eq + Hash, T3: DafnyType + Eq + Hash, T4: DafnyType + Eq + Hash, T5: DafnyType + Eq + Hash, T6: DafnyType + Eq + Hash, T7: DafnyType + Eq + Hash, T8: DafnyType + Eq + Hash, T9: DafnyType + Eq + Hash, T10: DafnyType + Eq + Hash, T11: DafnyType + Eq + Hash, T12: DafnyType + Eq + Hash, T13: DafnyType + Eq + Hash, T14: DafnyType + Eq + Hash, T15: DafnyType + Eq + Hash, T16: DafnyType + Eq + Hash> PartialEq
3067        for Tuple17<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15, T16> {
3068        fn eq(&self, other: &Self) -> bool {
3069            match (
3070                    self,
3071                    other
3072                ) {
3073                (Tuple17::_T17{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, }, Tuple17::_T17{_0: _2__0, _1: _2__1, _2: _2__2, _3: _2__3, _4: _2__4, _5: _2__5, _6: _2__6, _7: _2__7, _8: _2__8, _9: _2__9, _10: _2__10, _11: _2__11, _12: _2__12, _13: _2__13, _14: _2__14, _15: _2__15, _16: _2__16, }) => {
3074                    _0 == _2__0 && _1 == _2__1 && _2 == _2__2 && _3 == _2__3 && _4 == _2__4 && _5 == _2__5 && _6 == _2__6 && _7 == _2__7 && _8 == _2__8 && _9 == _2__9 && _10 == _2__10 && _11 == _2__11 && _12 == _2__12 && _13 == _2__13 && _14 == _2__14 && _15 == _2__15 && _16 == _2__16
3075                },
3076                _ => {
3077                    false
3078                },
3079            }
3080        }
3081    }
3082
3083    impl<T0: DafnyType + Eq + Hash, T1: DafnyType + Eq + Hash, T2: DafnyType + Eq + Hash, T3: DafnyType + Eq + Hash, T4: DafnyType + Eq + Hash, T5: DafnyType + Eq + Hash, T6: DafnyType + Eq + Hash, T7: DafnyType + Eq + Hash, T8: DafnyType + Eq + Hash, T9: DafnyType + Eq + Hash, T10: DafnyType + Eq + Hash, T11: DafnyType + Eq + Hash, T12: DafnyType + Eq + Hash, T13: DafnyType + Eq + Hash, T14: DafnyType + Eq + Hash, T15: DafnyType + Eq + Hash, T16: DafnyType + Eq + Hash> Eq
3084        for Tuple17<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15, T16> {}
3085
3086    impl<T0: DafnyType + Hash, T1: DafnyType + Hash, T2: DafnyType + Hash, T3: DafnyType + Hash, T4: DafnyType + Hash, T5: DafnyType + Hash, T6: DafnyType + Hash, T7: DafnyType + Hash, T8: DafnyType + Hash, T9: DafnyType + Hash, T10: DafnyType + Hash, T11: DafnyType + Hash, T12: DafnyType + Hash, T13: DafnyType + Hash, T14: DafnyType + Hash, T15: DafnyType + Hash, T16: DafnyType + Hash> Hash
3087        for Tuple17<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15, T16> {
3088        fn hash<_H: Hasher>(&self, _state: &mut _H) {
3089            match self {
3090                Tuple17::_T17{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, } => {
3091                    Hash::hash(_0, _state);
3092                    Hash::hash(_1, _state);
3093                    Hash::hash(_2, _state);
3094                    Hash::hash(_3, _state);
3095                    Hash::hash(_4, _state);
3096                    Hash::hash(_5, _state);
3097                    Hash::hash(_6, _state);
3098                    Hash::hash(_7, _state);
3099                    Hash::hash(_8, _state);
3100                    Hash::hash(_9, _state);
3101                    Hash::hash(_10, _state);
3102                    Hash::hash(_11, _state);
3103                    Hash::hash(_12, _state);
3104                    Hash::hash(_13, _state);
3105                    Hash::hash(_14, _state);
3106                    Hash::hash(_15, _state);
3107                    Hash::hash(_16, _state)
3108                },
3109            }
3110        }
3111    }
3112
3113    impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType, T9: DafnyType, T10: DafnyType, T11: DafnyType, T12: DafnyType, T13: DafnyType, T14: DafnyType, T15: DafnyType, T16: DafnyType> AsRef<Tuple17<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15, T16>>
3114        for Tuple17<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15, T16> {
3115        fn as_ref(&self) -> &Self {
3116            self
3117        }
3118    }
3119
3120    #[derive(Clone)]
3121    pub enum Tuple18<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType, T9: DafnyType, T10: DafnyType, T11: DafnyType, T12: DafnyType, T13: DafnyType, T14: DafnyType, T15: DafnyType, T16: DafnyType, T17: DafnyType> {
3122        _T18 {
3123            _0: T0,
3124            _1: T1,
3125            _2: T2,
3126            _3: T3,
3127            _4: T4,
3128            _5: T5,
3129            _6: T6,
3130            _7: T7,
3131            _8: T8,
3132            _9: T9,
3133            _10: T10,
3134            _11: T11,
3135            _12: T12,
3136            _13: T13,
3137            _14: T14,
3138            _15: T15,
3139            _16: T16,
3140            _17: T17
3141        }
3142    }
3143
3144    impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType, T9: DafnyType, T10: DafnyType, T11: DafnyType, T12: DafnyType, T13: DafnyType, T14: DafnyType, T15: DafnyType, T16: DafnyType, T17: DafnyType> Tuple18<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15, T16, T17> {
3145        /// Returns a borrow of the field _0
3146        pub fn _0(&self) -> &T0 {
3147            match self {
3148                Tuple18::_T18{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, } => _0,
3149            }
3150        }
3151        /// Returns a borrow of the field _1
3152        pub fn _1(&self) -> &T1 {
3153            match self {
3154                Tuple18::_T18{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, } => _1,
3155            }
3156        }
3157        /// Returns a borrow of the field _2
3158        pub fn _2(&self) -> &T2 {
3159            match self {
3160                Tuple18::_T18{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, } => _2,
3161            }
3162        }
3163        /// Returns a borrow of the field _3
3164        pub fn _3(&self) -> &T3 {
3165            match self {
3166                Tuple18::_T18{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, } => _3,
3167            }
3168        }
3169        /// Returns a borrow of the field _4
3170        pub fn _4(&self) -> &T4 {
3171            match self {
3172                Tuple18::_T18{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, } => _4,
3173            }
3174        }
3175        /// Returns a borrow of the field _5
3176        pub fn _5(&self) -> &T5 {
3177            match self {
3178                Tuple18::_T18{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, } => _5,
3179            }
3180        }
3181        /// Returns a borrow of the field _6
3182        pub fn _6(&self) -> &T6 {
3183            match self {
3184                Tuple18::_T18{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, } => _6,
3185            }
3186        }
3187        /// Returns a borrow of the field _7
3188        pub fn _7(&self) -> &T7 {
3189            match self {
3190                Tuple18::_T18{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, } => _7,
3191            }
3192        }
3193        /// Returns a borrow of the field _8
3194        pub fn _8(&self) -> &T8 {
3195            match self {
3196                Tuple18::_T18{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, } => _8,
3197            }
3198        }
3199        /// Returns a borrow of the field _9
3200        pub fn _9(&self) -> &T9 {
3201            match self {
3202                Tuple18::_T18{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, } => _9,
3203            }
3204        }
3205        /// Returns a borrow of the field _10
3206        pub fn _10(&self) -> &T10 {
3207            match self {
3208                Tuple18::_T18{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, } => _10,
3209            }
3210        }
3211        /// Returns a borrow of the field _11
3212        pub fn _11(&self) -> &T11 {
3213            match self {
3214                Tuple18::_T18{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, } => _11,
3215            }
3216        }
3217        /// Returns a borrow of the field _12
3218        pub fn _12(&self) -> &T12 {
3219            match self {
3220                Tuple18::_T18{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, } => _12,
3221            }
3222        }
3223        /// Returns a borrow of the field _13
3224        pub fn _13(&self) -> &T13 {
3225            match self {
3226                Tuple18::_T18{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, } => _13,
3227            }
3228        }
3229        /// Returns a borrow of the field _14
3230        pub fn _14(&self) -> &T14 {
3231            match self {
3232                Tuple18::_T18{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, } => _14,
3233            }
3234        }
3235        /// Returns a borrow of the field _15
3236        pub fn _15(&self) -> &T15 {
3237            match self {
3238                Tuple18::_T18{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, } => _15,
3239            }
3240        }
3241        /// Returns a borrow of the field _16
3242        pub fn _16(&self) -> &T16 {
3243            match self {
3244                Tuple18::_T18{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, } => _16,
3245            }
3246        }
3247        /// Returns a borrow of the field _17
3248        pub fn _17(&self) -> &T17 {
3249            match self {
3250                Tuple18::_T18{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, } => _17,
3251            }
3252        }
3253    }
3254
3255    impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType, T9: DafnyType, T10: DafnyType, T11: DafnyType, T12: DafnyType, T13: DafnyType, T14: DafnyType, T15: DafnyType, T16: DafnyType, T17: DafnyType> Debug
3256        for Tuple18<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15, T16, T17> {
3257        fn fmt(&self, f: &mut Formatter) -> Result {
3258            DafnyPrint::fmt_print(self, f, true)
3259        }
3260    }
3261
3262    impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType, T9: DafnyType, T10: DafnyType, T11: DafnyType, T12: DafnyType, T13: DafnyType, T14: DafnyType, T15: DafnyType, T16: DafnyType, T17: DafnyType> DafnyPrint
3263        for Tuple18<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15, T16, T17> {
3264        fn fmt_print(&self, _formatter: &mut Formatter, _in_seq: bool) -> std::fmt::Result {
3265            match self {
3266                Tuple18::_T18{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, } => {
3267                    write!(_formatter, "(")?;
3268                    DafnyPrint::fmt_print(_0, _formatter, false)?;
3269                    write!(_formatter, ", ")?;
3270                    DafnyPrint::fmt_print(_1, _formatter, false)?;
3271                    write!(_formatter, ", ")?;
3272                    DafnyPrint::fmt_print(_2, _formatter, false)?;
3273                    write!(_formatter, ", ")?;
3274                    DafnyPrint::fmt_print(_3, _formatter, false)?;
3275                    write!(_formatter, ", ")?;
3276                    DafnyPrint::fmt_print(_4, _formatter, false)?;
3277                    write!(_formatter, ", ")?;
3278                    DafnyPrint::fmt_print(_5, _formatter, false)?;
3279                    write!(_formatter, ", ")?;
3280                    DafnyPrint::fmt_print(_6, _formatter, false)?;
3281                    write!(_formatter, ", ")?;
3282                    DafnyPrint::fmt_print(_7, _formatter, false)?;
3283                    write!(_formatter, ", ")?;
3284                    DafnyPrint::fmt_print(_8, _formatter, false)?;
3285                    write!(_formatter, ", ")?;
3286                    DafnyPrint::fmt_print(_9, _formatter, false)?;
3287                    write!(_formatter, ", ")?;
3288                    DafnyPrint::fmt_print(_10, _formatter, false)?;
3289                    write!(_formatter, ", ")?;
3290                    DafnyPrint::fmt_print(_11, _formatter, false)?;
3291                    write!(_formatter, ", ")?;
3292                    DafnyPrint::fmt_print(_12, _formatter, false)?;
3293                    write!(_formatter, ", ")?;
3294                    DafnyPrint::fmt_print(_13, _formatter, false)?;
3295                    write!(_formatter, ", ")?;
3296                    DafnyPrint::fmt_print(_14, _formatter, false)?;
3297                    write!(_formatter, ", ")?;
3298                    DafnyPrint::fmt_print(_15, _formatter, false)?;
3299                    write!(_formatter, ", ")?;
3300                    DafnyPrint::fmt_print(_16, _formatter, false)?;
3301                    write!(_formatter, ", ")?;
3302                    DafnyPrint::fmt_print(_17, _formatter, false)?;
3303                    write!(_formatter, ")")?;
3304                    Ok(())
3305                },
3306            }
3307        }
3308    }
3309
3310    impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType, T9: DafnyType, T10: DafnyType, T11: DafnyType, T12: DafnyType, T13: DafnyType, T14: DafnyType, T15: DafnyType, T16: DafnyType, T17: DafnyType> Tuple18<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15, T16, T17> {
3311        /// Given type parameter conversions, returns a lambda to convert this structure
3312        pub fn coerce<__T0: DafnyType, __T1: DafnyType, __T2: DafnyType, __T3: DafnyType, __T4: DafnyType, __T5: DafnyType, __T6: DafnyType, __T7: DafnyType, __T8: DafnyType, __T9: DafnyType, __T10: DafnyType, __T11: DafnyType, __T12: DafnyType, __T13: DafnyType, __T14: DafnyType, __T15: DafnyType, __T16: DafnyType, __T17: DafnyType>(f_0: Rc<impl ::std::ops::Fn(T0) -> __T0 + 'static>, f_1: Rc<impl ::std::ops::Fn(T1) -> __T1 + 'static>, f_2: Rc<impl ::std::ops::Fn(T2) -> __T2 + 'static>, f_3: Rc<impl ::std::ops::Fn(T3) -> __T3 + 'static>, f_4: Rc<impl ::std::ops::Fn(T4) -> __T4 + 'static>, f_5: Rc<impl ::std::ops::Fn(T5) -> __T5 + 'static>, f_6: Rc<impl ::std::ops::Fn(T6) -> __T6 + 'static>, f_7: Rc<impl ::std::ops::Fn(T7) -> __T7 + 'static>, f_8: Rc<impl ::std::ops::Fn(T8) -> __T8 + 'static>, f_9: Rc<impl ::std::ops::Fn(T9) -> __T9 + 'static>, f_10: Rc<impl ::std::ops::Fn(T10) -> __T10 + 'static>, f_11: Rc<impl ::std::ops::Fn(T11) -> __T11 + 'static>, f_12: Rc<impl ::std::ops::Fn(T12) -> __T12 + 'static>, f_13: Rc<impl ::std::ops::Fn(T13) -> __T13 + 'static>, f_14: Rc<impl ::std::ops::Fn(T14) -> __T14 + 'static>, f_15: Rc<impl ::std::ops::Fn(T15) -> __T15 + 'static>, f_16: Rc<impl ::std::ops::Fn(T16) -> __T16 + 'static>, f_17: Rc<impl ::std::ops::Fn(T17) -> __T17 + 'static>) -> Rc<impl ::std::ops::Fn(Tuple18<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15, T16, T17>) -> Tuple18<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8, __T9, __T10, __T11, __T12, __T13, __T14, __T15, __T16, __T17>> {
3313            Rc::new(move |this: Self| -> Tuple18<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8, __T9, __T10, __T11, __T12, __T13, __T14, __T15, __T16, __T17>{
3314                    match this {
3315                        Tuple18::_T18{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, } => {
3316                            Tuple18::_T18 {
3317                                _0: f_0.clone()(_0),
3318                                _1: f_1.clone()(_1),
3319                                _2: f_2.clone()(_2),
3320                                _3: f_3.clone()(_3),
3321                                _4: f_4.clone()(_4),
3322                                _5: f_5.clone()(_5),
3323                                _6: f_6.clone()(_6),
3324                                _7: f_7.clone()(_7),
3325                                _8: f_8.clone()(_8),
3326                                _9: f_9.clone()(_9),
3327                                _10: f_10.clone()(_10),
3328                                _11: f_11.clone()(_11),
3329                                _12: f_12.clone()(_12),
3330                                _13: f_13.clone()(_13),
3331                                _14: f_14.clone()(_14),
3332                                _15: f_15.clone()(_15),
3333                                _16: f_16.clone()(_16),
3334                                _17: f_17.clone()(_17)
3335                            }
3336                        },
3337                    }
3338                })
3339        }
3340    }
3341
3342    impl<T0: DafnyType + Eq + Hash, T1: DafnyType + Eq + Hash, T2: DafnyType + Eq + Hash, T3: DafnyType + Eq + Hash, T4: DafnyType + Eq + Hash, T5: DafnyType + Eq + Hash, T6: DafnyType + Eq + Hash, T7: DafnyType + Eq + Hash, T8: DafnyType + Eq + Hash, T9: DafnyType + Eq + Hash, T10: DafnyType + Eq + Hash, T11: DafnyType + Eq + Hash, T12: DafnyType + Eq + Hash, T13: DafnyType + Eq + Hash, T14: DafnyType + Eq + Hash, T15: DafnyType + Eq + Hash, T16: DafnyType + Eq + Hash, T17: DafnyType + Eq + Hash> PartialEq
3343        for Tuple18<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15, T16, T17> {
3344        fn eq(&self, other: &Self) -> bool {
3345            match (
3346                    self,
3347                    other
3348                ) {
3349                (Tuple18::_T18{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, }, Tuple18::_T18{_0: _2__0, _1: _2__1, _2: _2__2, _3: _2__3, _4: _2__4, _5: _2__5, _6: _2__6, _7: _2__7, _8: _2__8, _9: _2__9, _10: _2__10, _11: _2__11, _12: _2__12, _13: _2__13, _14: _2__14, _15: _2__15, _16: _2__16, _17: _2__17, }) => {
3350                    _0 == _2__0 && _1 == _2__1 && _2 == _2__2 && _3 == _2__3 && _4 == _2__4 && _5 == _2__5 && _6 == _2__6 && _7 == _2__7 && _8 == _2__8 && _9 == _2__9 && _10 == _2__10 && _11 == _2__11 && _12 == _2__12 && _13 == _2__13 && _14 == _2__14 && _15 == _2__15 && _16 == _2__16 && _17 == _2__17
3351                },
3352                _ => {
3353                    false
3354                },
3355            }
3356        }
3357    }
3358
3359    impl<T0: DafnyType + Eq + Hash, T1: DafnyType + Eq + Hash, T2: DafnyType + Eq + Hash, T3: DafnyType + Eq + Hash, T4: DafnyType + Eq + Hash, T5: DafnyType + Eq + Hash, T6: DafnyType + Eq + Hash, T7: DafnyType + Eq + Hash, T8: DafnyType + Eq + Hash, T9: DafnyType + Eq + Hash, T10: DafnyType + Eq + Hash, T11: DafnyType + Eq + Hash, T12: DafnyType + Eq + Hash, T13: DafnyType + Eq + Hash, T14: DafnyType + Eq + Hash, T15: DafnyType + Eq + Hash, T16: DafnyType + Eq + Hash, T17: DafnyType + Eq + Hash> Eq
3360        for Tuple18<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15, T16, T17> {}
3361
3362    impl<T0: DafnyType + Hash, T1: DafnyType + Hash, T2: DafnyType + Hash, T3: DafnyType + Hash, T4: DafnyType + Hash, T5: DafnyType + Hash, T6: DafnyType + Hash, T7: DafnyType + Hash, T8: DafnyType + Hash, T9: DafnyType + Hash, T10: DafnyType + Hash, T11: DafnyType + Hash, T12: DafnyType + Hash, T13: DafnyType + Hash, T14: DafnyType + Hash, T15: DafnyType + Hash, T16: DafnyType + Hash, T17: DafnyType + Hash> Hash
3363        for Tuple18<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15, T16, T17> {
3364        fn hash<_H: Hasher>(&self, _state: &mut _H) {
3365            match self {
3366                Tuple18::_T18{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, } => {
3367                    Hash::hash(_0, _state);
3368                    Hash::hash(_1, _state);
3369                    Hash::hash(_2, _state);
3370                    Hash::hash(_3, _state);
3371                    Hash::hash(_4, _state);
3372                    Hash::hash(_5, _state);
3373                    Hash::hash(_6, _state);
3374                    Hash::hash(_7, _state);
3375                    Hash::hash(_8, _state);
3376                    Hash::hash(_9, _state);
3377                    Hash::hash(_10, _state);
3378                    Hash::hash(_11, _state);
3379                    Hash::hash(_12, _state);
3380                    Hash::hash(_13, _state);
3381                    Hash::hash(_14, _state);
3382                    Hash::hash(_15, _state);
3383                    Hash::hash(_16, _state);
3384                    Hash::hash(_17, _state)
3385                },
3386            }
3387        }
3388    }
3389
3390    impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType, T9: DafnyType, T10: DafnyType, T11: DafnyType, T12: DafnyType, T13: DafnyType, T14: DafnyType, T15: DafnyType, T16: DafnyType, T17: DafnyType> AsRef<Tuple18<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15, T16, T17>>
3391        for Tuple18<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15, T16, T17> {
3392        fn as_ref(&self) -> &Self {
3393            self
3394        }
3395    }
3396
3397    #[derive(Clone)]
3398    pub enum Tuple19<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType, T9: DafnyType, T10: DafnyType, T11: DafnyType, T12: DafnyType, T13: DafnyType, T14: DafnyType, T15: DafnyType, T16: DafnyType, T17: DafnyType, T18: DafnyType> {
3399        _T19 {
3400            _0: T0,
3401            _1: T1,
3402            _2: T2,
3403            _3: T3,
3404            _4: T4,
3405            _5: T5,
3406            _6: T6,
3407            _7: T7,
3408            _8: T8,
3409            _9: T9,
3410            _10: T10,
3411            _11: T11,
3412            _12: T12,
3413            _13: T13,
3414            _14: T14,
3415            _15: T15,
3416            _16: T16,
3417            _17: T17,
3418            _18: T18
3419        }
3420    }
3421
3422    impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType, T9: DafnyType, T10: DafnyType, T11: DafnyType, T12: DafnyType, T13: DafnyType, T14: DafnyType, T15: DafnyType, T16: DafnyType, T17: DafnyType, T18: DafnyType> Tuple19<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15, T16, T17, T18> {
3423        /// Returns a borrow of the field _0
3424        pub fn _0(&self) -> &T0 {
3425            match self {
3426                Tuple19::_T19{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, } => _0,
3427            }
3428        }
3429        /// Returns a borrow of the field _1
3430        pub fn _1(&self) -> &T1 {
3431            match self {
3432                Tuple19::_T19{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, } => _1,
3433            }
3434        }
3435        /// Returns a borrow of the field _2
3436        pub fn _2(&self) -> &T2 {
3437            match self {
3438                Tuple19::_T19{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, } => _2,
3439            }
3440        }
3441        /// Returns a borrow of the field _3
3442        pub fn _3(&self) -> &T3 {
3443            match self {
3444                Tuple19::_T19{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, } => _3,
3445            }
3446        }
3447        /// Returns a borrow of the field _4
3448        pub fn _4(&self) -> &T4 {
3449            match self {
3450                Tuple19::_T19{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, } => _4,
3451            }
3452        }
3453        /// Returns a borrow of the field _5
3454        pub fn _5(&self) -> &T5 {
3455            match self {
3456                Tuple19::_T19{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, } => _5,
3457            }
3458        }
3459        /// Returns a borrow of the field _6
3460        pub fn _6(&self) -> &T6 {
3461            match self {
3462                Tuple19::_T19{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, } => _6,
3463            }
3464        }
3465        /// Returns a borrow of the field _7
3466        pub fn _7(&self) -> &T7 {
3467            match self {
3468                Tuple19::_T19{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, } => _7,
3469            }
3470        }
3471        /// Returns a borrow of the field _8
3472        pub fn _8(&self) -> &T8 {
3473            match self {
3474                Tuple19::_T19{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, } => _8,
3475            }
3476        }
3477        /// Returns a borrow of the field _9
3478        pub fn _9(&self) -> &T9 {
3479            match self {
3480                Tuple19::_T19{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, } => _9,
3481            }
3482        }
3483        /// Returns a borrow of the field _10
3484        pub fn _10(&self) -> &T10 {
3485            match self {
3486                Tuple19::_T19{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, } => _10,
3487            }
3488        }
3489        /// Returns a borrow of the field _11
3490        pub fn _11(&self) -> &T11 {
3491            match self {
3492                Tuple19::_T19{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, } => _11,
3493            }
3494        }
3495        /// Returns a borrow of the field _12
3496        pub fn _12(&self) -> &T12 {
3497            match self {
3498                Tuple19::_T19{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, } => _12,
3499            }
3500        }
3501        /// Returns a borrow of the field _13
3502        pub fn _13(&self) -> &T13 {
3503            match self {
3504                Tuple19::_T19{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, } => _13,
3505            }
3506        }
3507        /// Returns a borrow of the field _14
3508        pub fn _14(&self) -> &T14 {
3509            match self {
3510                Tuple19::_T19{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, } => _14,
3511            }
3512        }
3513        /// Returns a borrow of the field _15
3514        pub fn _15(&self) -> &T15 {
3515            match self {
3516                Tuple19::_T19{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, } => _15,
3517            }
3518        }
3519        /// Returns a borrow of the field _16
3520        pub fn _16(&self) -> &T16 {
3521            match self {
3522                Tuple19::_T19{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, } => _16,
3523            }
3524        }
3525        /// Returns a borrow of the field _17
3526        pub fn _17(&self) -> &T17 {
3527            match self {
3528                Tuple19::_T19{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, } => _17,
3529            }
3530        }
3531        /// Returns a borrow of the field _18
3532        pub fn _18(&self) -> &T18 {
3533            match self {
3534                Tuple19::_T19{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, } => _18,
3535            }
3536        }
3537    }
3538
3539    impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType, T9: DafnyType, T10: DafnyType, T11: DafnyType, T12: DafnyType, T13: DafnyType, T14: DafnyType, T15: DafnyType, T16: DafnyType, T17: DafnyType, T18: DafnyType> Debug
3540        for Tuple19<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15, T16, T17, T18> {
3541        fn fmt(&self, f: &mut Formatter) -> Result {
3542            DafnyPrint::fmt_print(self, f, true)
3543        }
3544    }
3545
3546    impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType, T9: DafnyType, T10: DafnyType, T11: DafnyType, T12: DafnyType, T13: DafnyType, T14: DafnyType, T15: DafnyType, T16: DafnyType, T17: DafnyType, T18: DafnyType> DafnyPrint
3547        for Tuple19<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15, T16, T17, T18> {
3548        fn fmt_print(&self, _formatter: &mut Formatter, _in_seq: bool) -> std::fmt::Result {
3549            match self {
3550                Tuple19::_T19{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, } => {
3551                    write!(_formatter, "(")?;
3552                    DafnyPrint::fmt_print(_0, _formatter, false)?;
3553                    write!(_formatter, ", ")?;
3554                    DafnyPrint::fmt_print(_1, _formatter, false)?;
3555                    write!(_formatter, ", ")?;
3556                    DafnyPrint::fmt_print(_2, _formatter, false)?;
3557                    write!(_formatter, ", ")?;
3558                    DafnyPrint::fmt_print(_3, _formatter, false)?;
3559                    write!(_formatter, ", ")?;
3560                    DafnyPrint::fmt_print(_4, _formatter, false)?;
3561                    write!(_formatter, ", ")?;
3562                    DafnyPrint::fmt_print(_5, _formatter, false)?;
3563                    write!(_formatter, ", ")?;
3564                    DafnyPrint::fmt_print(_6, _formatter, false)?;
3565                    write!(_formatter, ", ")?;
3566                    DafnyPrint::fmt_print(_7, _formatter, false)?;
3567                    write!(_formatter, ", ")?;
3568                    DafnyPrint::fmt_print(_8, _formatter, false)?;
3569                    write!(_formatter, ", ")?;
3570                    DafnyPrint::fmt_print(_9, _formatter, false)?;
3571                    write!(_formatter, ", ")?;
3572                    DafnyPrint::fmt_print(_10, _formatter, false)?;
3573                    write!(_formatter, ", ")?;
3574                    DafnyPrint::fmt_print(_11, _formatter, false)?;
3575                    write!(_formatter, ", ")?;
3576                    DafnyPrint::fmt_print(_12, _formatter, false)?;
3577                    write!(_formatter, ", ")?;
3578                    DafnyPrint::fmt_print(_13, _formatter, false)?;
3579                    write!(_formatter, ", ")?;
3580                    DafnyPrint::fmt_print(_14, _formatter, false)?;
3581                    write!(_formatter, ", ")?;
3582                    DafnyPrint::fmt_print(_15, _formatter, false)?;
3583                    write!(_formatter, ", ")?;
3584                    DafnyPrint::fmt_print(_16, _formatter, false)?;
3585                    write!(_formatter, ", ")?;
3586                    DafnyPrint::fmt_print(_17, _formatter, false)?;
3587                    write!(_formatter, ", ")?;
3588                    DafnyPrint::fmt_print(_18, _formatter, false)?;
3589                    write!(_formatter, ")")?;
3590                    Ok(())
3591                },
3592            }
3593        }
3594    }
3595
3596    impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType, T9: DafnyType, T10: DafnyType, T11: DafnyType, T12: DafnyType, T13: DafnyType, T14: DafnyType, T15: DafnyType, T16: DafnyType, T17: DafnyType, T18: DafnyType> Tuple19<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15, T16, T17, T18> {
3597        /// Given type parameter conversions, returns a lambda to convert this structure
3598        pub fn coerce<__T0: DafnyType, __T1: DafnyType, __T2: DafnyType, __T3: DafnyType, __T4: DafnyType, __T5: DafnyType, __T6: DafnyType, __T7: DafnyType, __T8: DafnyType, __T9: DafnyType, __T10: DafnyType, __T11: DafnyType, __T12: DafnyType, __T13: DafnyType, __T14: DafnyType, __T15: DafnyType, __T16: DafnyType, __T17: DafnyType, __T18: DafnyType>(f_0: Rc<impl ::std::ops::Fn(T0) -> __T0 + 'static>, f_1: Rc<impl ::std::ops::Fn(T1) -> __T1 + 'static>, f_2: Rc<impl ::std::ops::Fn(T2) -> __T2 + 'static>, f_3: Rc<impl ::std::ops::Fn(T3) -> __T3 + 'static>, f_4: Rc<impl ::std::ops::Fn(T4) -> __T4 + 'static>, f_5: Rc<impl ::std::ops::Fn(T5) -> __T5 + 'static>, f_6: Rc<impl ::std::ops::Fn(T6) -> __T6 + 'static>, f_7: Rc<impl ::std::ops::Fn(T7) -> __T7 + 'static>, f_8: Rc<impl ::std::ops::Fn(T8) -> __T8 + 'static>, f_9: Rc<impl ::std::ops::Fn(T9) -> __T9 + 'static>, f_10: Rc<impl ::std::ops::Fn(T10) -> __T10 + 'static>, f_11: Rc<impl ::std::ops::Fn(T11) -> __T11 + 'static>, f_12: Rc<impl ::std::ops::Fn(T12) -> __T12 + 'static>, f_13: Rc<impl ::std::ops::Fn(T13) -> __T13 + 'static>, f_14: Rc<impl ::std::ops::Fn(T14) -> __T14 + 'static>, f_15: Rc<impl ::std::ops::Fn(T15) -> __T15 + 'static>, f_16: Rc<impl ::std::ops::Fn(T16) -> __T16 + 'static>, f_17: Rc<impl ::std::ops::Fn(T17) -> __T17 + 'static>, f_18: Rc<impl ::std::ops::Fn(T18) -> __T18 + 'static>) -> Rc<impl ::std::ops::Fn(Tuple19<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15, T16, T17, T18>) -> Tuple19<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8, __T9, __T10, __T11, __T12, __T13, __T14, __T15, __T16, __T17, __T18>> {
3599            Rc::new(move |this: Self| -> Tuple19<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8, __T9, __T10, __T11, __T12, __T13, __T14, __T15, __T16, __T17, __T18>{
3600                    match this {
3601                        Tuple19::_T19{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, } => {
3602                            Tuple19::_T19 {
3603                                _0: f_0.clone()(_0),
3604                                _1: f_1.clone()(_1),
3605                                _2: f_2.clone()(_2),
3606                                _3: f_3.clone()(_3),
3607                                _4: f_4.clone()(_4),
3608                                _5: f_5.clone()(_5),
3609                                _6: f_6.clone()(_6),
3610                                _7: f_7.clone()(_7),
3611                                _8: f_8.clone()(_8),
3612                                _9: f_9.clone()(_9),
3613                                _10: f_10.clone()(_10),
3614                                _11: f_11.clone()(_11),
3615                                _12: f_12.clone()(_12),
3616                                _13: f_13.clone()(_13),
3617                                _14: f_14.clone()(_14),
3618                                _15: f_15.clone()(_15),
3619                                _16: f_16.clone()(_16),
3620                                _17: f_17.clone()(_17),
3621                                _18: f_18.clone()(_18)
3622                            }
3623                        },
3624                    }
3625                })
3626        }
3627    }
3628
3629    impl<T0: DafnyType + Eq + Hash, T1: DafnyType + Eq + Hash, T2: DafnyType + Eq + Hash, T3: DafnyType + Eq + Hash, T4: DafnyType + Eq + Hash, T5: DafnyType + Eq + Hash, T6: DafnyType + Eq + Hash, T7: DafnyType + Eq + Hash, T8: DafnyType + Eq + Hash, T9: DafnyType + Eq + Hash, T10: DafnyType + Eq + Hash, T11: DafnyType + Eq + Hash, T12: DafnyType + Eq + Hash, T13: DafnyType + Eq + Hash, T14: DafnyType + Eq + Hash, T15: DafnyType + Eq + Hash, T16: DafnyType + Eq + Hash, T17: DafnyType + Eq + Hash, T18: DafnyType + Eq + Hash> PartialEq
3630        for Tuple19<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15, T16, T17, T18> {
3631        fn eq(&self, other: &Self) -> bool {
3632            match (
3633                    self,
3634                    other
3635                ) {
3636                (Tuple19::_T19{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, }, Tuple19::_T19{_0: _2__0, _1: _2__1, _2: _2__2, _3: _2__3, _4: _2__4, _5: _2__5, _6: _2__6, _7: _2__7, _8: _2__8, _9: _2__9, _10: _2__10, _11: _2__11, _12: _2__12, _13: _2__13, _14: _2__14, _15: _2__15, _16: _2__16, _17: _2__17, _18: _2__18, }) => {
3637                    _0 == _2__0 && _1 == _2__1 && _2 == _2__2 && _3 == _2__3 && _4 == _2__4 && _5 == _2__5 && _6 == _2__6 && _7 == _2__7 && _8 == _2__8 && _9 == _2__9 && _10 == _2__10 && _11 == _2__11 && _12 == _2__12 && _13 == _2__13 && _14 == _2__14 && _15 == _2__15 && _16 == _2__16 && _17 == _2__17 && _18 == _2__18
3638                },
3639                _ => {
3640                    false
3641                },
3642            }
3643        }
3644    }
3645
3646    impl<T0: DafnyType + Eq + Hash, T1: DafnyType + Eq + Hash, T2: DafnyType + Eq + Hash, T3: DafnyType + Eq + Hash, T4: DafnyType + Eq + Hash, T5: DafnyType + Eq + Hash, T6: DafnyType + Eq + Hash, T7: DafnyType + Eq + Hash, T8: DafnyType + Eq + Hash, T9: DafnyType + Eq + Hash, T10: DafnyType + Eq + Hash, T11: DafnyType + Eq + Hash, T12: DafnyType + Eq + Hash, T13: DafnyType + Eq + Hash, T14: DafnyType + Eq + Hash, T15: DafnyType + Eq + Hash, T16: DafnyType + Eq + Hash, T17: DafnyType + Eq + Hash, T18: DafnyType + Eq + Hash> Eq
3647        for Tuple19<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15, T16, T17, T18> {}
3648
3649    impl<T0: DafnyType + Hash, T1: DafnyType + Hash, T2: DafnyType + Hash, T3: DafnyType + Hash, T4: DafnyType + Hash, T5: DafnyType + Hash, T6: DafnyType + Hash, T7: DafnyType + Hash, T8: DafnyType + Hash, T9: DafnyType + Hash, T10: DafnyType + Hash, T11: DafnyType + Hash, T12: DafnyType + Hash, T13: DafnyType + Hash, T14: DafnyType + Hash, T15: DafnyType + Hash, T16: DafnyType + Hash, T17: DafnyType + Hash, T18: DafnyType + Hash> Hash
3650        for Tuple19<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15, T16, T17, T18> {
3651        fn hash<_H: Hasher>(&self, _state: &mut _H) {
3652            match self {
3653                Tuple19::_T19{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, } => {
3654                    Hash::hash(_0, _state);
3655                    Hash::hash(_1, _state);
3656                    Hash::hash(_2, _state);
3657                    Hash::hash(_3, _state);
3658                    Hash::hash(_4, _state);
3659                    Hash::hash(_5, _state);
3660                    Hash::hash(_6, _state);
3661                    Hash::hash(_7, _state);
3662                    Hash::hash(_8, _state);
3663                    Hash::hash(_9, _state);
3664                    Hash::hash(_10, _state);
3665                    Hash::hash(_11, _state);
3666                    Hash::hash(_12, _state);
3667                    Hash::hash(_13, _state);
3668                    Hash::hash(_14, _state);
3669                    Hash::hash(_15, _state);
3670                    Hash::hash(_16, _state);
3671                    Hash::hash(_17, _state);
3672                    Hash::hash(_18, _state)
3673                },
3674            }
3675        }
3676    }
3677
3678    impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType, T9: DafnyType, T10: DafnyType, T11: DafnyType, T12: DafnyType, T13: DafnyType, T14: DafnyType, T15: DafnyType, T16: DafnyType, T17: DafnyType, T18: DafnyType> AsRef<Tuple19<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15, T16, T17, T18>>
3679        for Tuple19<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15, T16, T17, T18> {
3680        fn as_ref(&self) -> &Self {
3681            self
3682        }
3683    }
3684
3685    #[derive(Clone)]
3686    pub enum Tuple20<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType, T9: DafnyType, T10: DafnyType, T11: DafnyType, T12: DafnyType, T13: DafnyType, T14: DafnyType, T15: DafnyType, T16: DafnyType, T17: DafnyType, T18: DafnyType, T19: DafnyType> {
3687        _T20 {
3688            _0: T0,
3689            _1: T1,
3690            _2: T2,
3691            _3: T3,
3692            _4: T4,
3693            _5: T5,
3694            _6: T6,
3695            _7: T7,
3696            _8: T8,
3697            _9: T9,
3698            _10: T10,
3699            _11: T11,
3700            _12: T12,
3701            _13: T13,
3702            _14: T14,
3703            _15: T15,
3704            _16: T16,
3705            _17: T17,
3706            _18: T18,
3707            _19: T19
3708        }
3709    }
3710
3711    impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType, T9: DafnyType, T10: DafnyType, T11: DafnyType, T12: DafnyType, T13: DafnyType, T14: DafnyType, T15: DafnyType, T16: DafnyType, T17: DafnyType, T18: DafnyType, T19: DafnyType> Tuple20<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15, T16, T17, T18, T19> {
3712        /// Returns a borrow of the field _0
3713        pub fn _0(&self) -> &T0 {
3714            match self {
3715                Tuple20::_T20{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, _19, } => _0,
3716            }
3717        }
3718        /// Returns a borrow of the field _1
3719        pub fn _1(&self) -> &T1 {
3720            match self {
3721                Tuple20::_T20{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, _19, } => _1,
3722            }
3723        }
3724        /// Returns a borrow of the field _2
3725        pub fn _2(&self) -> &T2 {
3726            match self {
3727                Tuple20::_T20{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, _19, } => _2,
3728            }
3729        }
3730        /// Returns a borrow of the field _3
3731        pub fn _3(&self) -> &T3 {
3732            match self {
3733                Tuple20::_T20{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, _19, } => _3,
3734            }
3735        }
3736        /// Returns a borrow of the field _4
3737        pub fn _4(&self) -> &T4 {
3738            match self {
3739                Tuple20::_T20{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, _19, } => _4,
3740            }
3741        }
3742        /// Returns a borrow of the field _5
3743        pub fn _5(&self) -> &T5 {
3744            match self {
3745                Tuple20::_T20{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, _19, } => _5,
3746            }
3747        }
3748        /// Returns a borrow of the field _6
3749        pub fn _6(&self) -> &T6 {
3750            match self {
3751                Tuple20::_T20{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, _19, } => _6,
3752            }
3753        }
3754        /// Returns a borrow of the field _7
3755        pub fn _7(&self) -> &T7 {
3756            match self {
3757                Tuple20::_T20{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, _19, } => _7,
3758            }
3759        }
3760        /// Returns a borrow of the field _8
3761        pub fn _8(&self) -> &T8 {
3762            match self {
3763                Tuple20::_T20{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, _19, } => _8,
3764            }
3765        }
3766        /// Returns a borrow of the field _9
3767        pub fn _9(&self) -> &T9 {
3768            match self {
3769                Tuple20::_T20{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, _19, } => _9,
3770            }
3771        }
3772        /// Returns a borrow of the field _10
3773        pub fn _10(&self) -> &T10 {
3774            match self {
3775                Tuple20::_T20{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, _19, } => _10,
3776            }
3777        }
3778        /// Returns a borrow of the field _11
3779        pub fn _11(&self) -> &T11 {
3780            match self {
3781                Tuple20::_T20{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, _19, } => _11,
3782            }
3783        }
3784        /// Returns a borrow of the field _12
3785        pub fn _12(&self) -> &T12 {
3786            match self {
3787                Tuple20::_T20{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, _19, } => _12,
3788            }
3789        }
3790        /// Returns a borrow of the field _13
3791        pub fn _13(&self) -> &T13 {
3792            match self {
3793                Tuple20::_T20{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, _19, } => _13,
3794            }
3795        }
3796        /// Returns a borrow of the field _14
3797        pub fn _14(&self) -> &T14 {
3798            match self {
3799                Tuple20::_T20{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, _19, } => _14,
3800            }
3801        }
3802        /// Returns a borrow of the field _15
3803        pub fn _15(&self) -> &T15 {
3804            match self {
3805                Tuple20::_T20{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, _19, } => _15,
3806            }
3807        }
3808        /// Returns a borrow of the field _16
3809        pub fn _16(&self) -> &T16 {
3810            match self {
3811                Tuple20::_T20{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, _19, } => _16,
3812            }
3813        }
3814        /// Returns a borrow of the field _17
3815        pub fn _17(&self) -> &T17 {
3816            match self {
3817                Tuple20::_T20{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, _19, } => _17,
3818            }
3819        }
3820        /// Returns a borrow of the field _18
3821        pub fn _18(&self) -> &T18 {
3822            match self {
3823                Tuple20::_T20{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, _19, } => _18,
3824            }
3825        }
3826        /// Returns a borrow of the field _19
3827        pub fn _19(&self) -> &T19 {
3828            match self {
3829                Tuple20::_T20{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, _19, } => _19,
3830            }
3831        }
3832    }
3833
3834    impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType, T9: DafnyType, T10: DafnyType, T11: DafnyType, T12: DafnyType, T13: DafnyType, T14: DafnyType, T15: DafnyType, T16: DafnyType, T17: DafnyType, T18: DafnyType, T19: DafnyType> Debug
3835        for Tuple20<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15, T16, T17, T18, T19> {
3836        fn fmt(&self, f: &mut Formatter) -> Result {
3837            DafnyPrint::fmt_print(self, f, true)
3838        }
3839    }
3840
3841    impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType, T9: DafnyType, T10: DafnyType, T11: DafnyType, T12: DafnyType, T13: DafnyType, T14: DafnyType, T15: DafnyType, T16: DafnyType, T17: DafnyType, T18: DafnyType, T19: DafnyType> DafnyPrint
3842        for Tuple20<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15, T16, T17, T18, T19> {
3843        fn fmt_print(&self, _formatter: &mut Formatter, _in_seq: bool) -> std::fmt::Result {
3844            match self {
3845                Tuple20::_T20{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, _19, } => {
3846                    write!(_formatter, "(")?;
3847                    DafnyPrint::fmt_print(_0, _formatter, false)?;
3848                    write!(_formatter, ", ")?;
3849                    DafnyPrint::fmt_print(_1, _formatter, false)?;
3850                    write!(_formatter, ", ")?;
3851                    DafnyPrint::fmt_print(_2, _formatter, false)?;
3852                    write!(_formatter, ", ")?;
3853                    DafnyPrint::fmt_print(_3, _formatter, false)?;
3854                    write!(_formatter, ", ")?;
3855                    DafnyPrint::fmt_print(_4, _formatter, false)?;
3856                    write!(_formatter, ", ")?;
3857                    DafnyPrint::fmt_print(_5, _formatter, false)?;
3858                    write!(_formatter, ", ")?;
3859                    DafnyPrint::fmt_print(_6, _formatter, false)?;
3860                    write!(_formatter, ", ")?;
3861                    DafnyPrint::fmt_print(_7, _formatter, false)?;
3862                    write!(_formatter, ", ")?;
3863                    DafnyPrint::fmt_print(_8, _formatter, false)?;
3864                    write!(_formatter, ", ")?;
3865                    DafnyPrint::fmt_print(_9, _formatter, false)?;
3866                    write!(_formatter, ", ")?;
3867                    DafnyPrint::fmt_print(_10, _formatter, false)?;
3868                    write!(_formatter, ", ")?;
3869                    DafnyPrint::fmt_print(_11, _formatter, false)?;
3870                    write!(_formatter, ", ")?;
3871                    DafnyPrint::fmt_print(_12, _formatter, false)?;
3872                    write!(_formatter, ", ")?;
3873                    DafnyPrint::fmt_print(_13, _formatter, false)?;
3874                    write!(_formatter, ", ")?;
3875                    DafnyPrint::fmt_print(_14, _formatter, false)?;
3876                    write!(_formatter, ", ")?;
3877                    DafnyPrint::fmt_print(_15, _formatter, false)?;
3878                    write!(_formatter, ", ")?;
3879                    DafnyPrint::fmt_print(_16, _formatter, false)?;
3880                    write!(_formatter, ", ")?;
3881                    DafnyPrint::fmt_print(_17, _formatter, false)?;
3882                    write!(_formatter, ", ")?;
3883                    DafnyPrint::fmt_print(_18, _formatter, false)?;
3884                    write!(_formatter, ", ")?;
3885                    DafnyPrint::fmt_print(_19, _formatter, false)?;
3886                    write!(_formatter, ")")?;
3887                    Ok(())
3888                },
3889            }
3890        }
3891    }
3892
3893    impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType, T9: DafnyType, T10: DafnyType, T11: DafnyType, T12: DafnyType, T13: DafnyType, T14: DafnyType, T15: DafnyType, T16: DafnyType, T17: DafnyType, T18: DafnyType, T19: DafnyType> Tuple20<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15, T16, T17, T18, T19> {
3894        /// Given type parameter conversions, returns a lambda to convert this structure
3895        pub fn coerce<__T0: DafnyType, __T1: DafnyType, __T2: DafnyType, __T3: DafnyType, __T4: DafnyType, __T5: DafnyType, __T6: DafnyType, __T7: DafnyType, __T8: DafnyType, __T9: DafnyType, __T10: DafnyType, __T11: DafnyType, __T12: DafnyType, __T13: DafnyType, __T14: DafnyType, __T15: DafnyType, __T16: DafnyType, __T17: DafnyType, __T18: DafnyType, __T19: DafnyType>(f_0: Rc<impl ::std::ops::Fn(T0) -> __T0 + 'static>, f_1: Rc<impl ::std::ops::Fn(T1) -> __T1 + 'static>, f_2: Rc<impl ::std::ops::Fn(T2) -> __T2 + 'static>, f_3: Rc<impl ::std::ops::Fn(T3) -> __T3 + 'static>, f_4: Rc<impl ::std::ops::Fn(T4) -> __T4 + 'static>, f_5: Rc<impl ::std::ops::Fn(T5) -> __T5 + 'static>, f_6: Rc<impl ::std::ops::Fn(T6) -> __T6 + 'static>, f_7: Rc<impl ::std::ops::Fn(T7) -> __T7 + 'static>, f_8: Rc<impl ::std::ops::Fn(T8) -> __T8 + 'static>, f_9: Rc<impl ::std::ops::Fn(T9) -> __T9 + 'static>, f_10: Rc<impl ::std::ops::Fn(T10) -> __T10 + 'static>, f_11: Rc<impl ::std::ops::Fn(T11) -> __T11 + 'static>, f_12: Rc<impl ::std::ops::Fn(T12) -> __T12 + 'static>, f_13: Rc<impl ::std::ops::Fn(T13) -> __T13 + 'static>, f_14: Rc<impl ::std::ops::Fn(T14) -> __T14 + 'static>, f_15: Rc<impl ::std::ops::Fn(T15) -> __T15 + 'static>, f_16: Rc<impl ::std::ops::Fn(T16) -> __T16 + 'static>, f_17: Rc<impl ::std::ops::Fn(T17) -> __T17 + 'static>, f_18: Rc<impl ::std::ops::Fn(T18) -> __T18 + 'static>, f_19: Rc<impl ::std::ops::Fn(T19) -> __T19 + 'static>) -> Rc<impl ::std::ops::Fn(Tuple20<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15, T16, T17, T18, T19>) -> Tuple20<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8, __T9, __T10, __T11, __T12, __T13, __T14, __T15, __T16, __T17, __T18, __T19>> {
3896            Rc::new(move |this: Self| -> Tuple20<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8, __T9, __T10, __T11, __T12, __T13, __T14, __T15, __T16, __T17, __T18, __T19>{
3897                    match this {
3898                        Tuple20::_T20{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, _19, } => {
3899                            Tuple20::_T20 {
3900                                _0: f_0.clone()(_0),
3901                                _1: f_1.clone()(_1),
3902                                _2: f_2.clone()(_2),
3903                                _3: f_3.clone()(_3),
3904                                _4: f_4.clone()(_4),
3905                                _5: f_5.clone()(_5),
3906                                _6: f_6.clone()(_6),
3907                                _7: f_7.clone()(_7),
3908                                _8: f_8.clone()(_8),
3909                                _9: f_9.clone()(_9),
3910                                _10: f_10.clone()(_10),
3911                                _11: f_11.clone()(_11),
3912                                _12: f_12.clone()(_12),
3913                                _13: f_13.clone()(_13),
3914                                _14: f_14.clone()(_14),
3915                                _15: f_15.clone()(_15),
3916                                _16: f_16.clone()(_16),
3917                                _17: f_17.clone()(_17),
3918                                _18: f_18.clone()(_18),
3919                                _19: f_19.clone()(_19)
3920                            }
3921                        },
3922                    }
3923                })
3924        }
3925    }
3926
3927    impl<T0: DafnyType + Eq + Hash, T1: DafnyType + Eq + Hash, T2: DafnyType + Eq + Hash, T3: DafnyType + Eq + Hash, T4: DafnyType + Eq + Hash, T5: DafnyType + Eq + Hash, T6: DafnyType + Eq + Hash, T7: DafnyType + Eq + Hash, T8: DafnyType + Eq + Hash, T9: DafnyType + Eq + Hash, T10: DafnyType + Eq + Hash, T11: DafnyType + Eq + Hash, T12: DafnyType + Eq + Hash, T13: DafnyType + Eq + Hash, T14: DafnyType + Eq + Hash, T15: DafnyType + Eq + Hash, T16: DafnyType + Eq + Hash, T17: DafnyType + Eq + Hash, T18: DafnyType + Eq + Hash, T19: DafnyType + Eq + Hash> PartialEq
3928        for Tuple20<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15, T16, T17, T18, T19> {
3929        fn eq(&self, other: &Self) -> bool {
3930            match (
3931                    self,
3932                    other
3933                ) {
3934                (Tuple20::_T20{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, _19, }, Tuple20::_T20{_0: _2__0, _1: _2__1, _2: _2__2, _3: _2__3, _4: _2__4, _5: _2__5, _6: _2__6, _7: _2__7, _8: _2__8, _9: _2__9, _10: _2__10, _11: _2__11, _12: _2__12, _13: _2__13, _14: _2__14, _15: _2__15, _16: _2__16, _17: _2__17, _18: _2__18, _19: _2__19, }) => {
3935                    _0 == _2__0 && _1 == _2__1 && _2 == _2__2 && _3 == _2__3 && _4 == _2__4 && _5 == _2__5 && _6 == _2__6 && _7 == _2__7 && _8 == _2__8 && _9 == _2__9 && _10 == _2__10 && _11 == _2__11 && _12 == _2__12 && _13 == _2__13 && _14 == _2__14 && _15 == _2__15 && _16 == _2__16 && _17 == _2__17 && _18 == _2__18 && _19 == _2__19
3936                },
3937                _ => {
3938                    false
3939                },
3940            }
3941        }
3942    }
3943
3944    impl<T0: DafnyType + Eq + Hash, T1: DafnyType + Eq + Hash, T2: DafnyType + Eq + Hash, T3: DafnyType + Eq + Hash, T4: DafnyType + Eq + Hash, T5: DafnyType + Eq + Hash, T6: DafnyType + Eq + Hash, T7: DafnyType + Eq + Hash, T8: DafnyType + Eq + Hash, T9: DafnyType + Eq + Hash, T10: DafnyType + Eq + Hash, T11: DafnyType + Eq + Hash, T12: DafnyType + Eq + Hash, T13: DafnyType + Eq + Hash, T14: DafnyType + Eq + Hash, T15: DafnyType + Eq + Hash, T16: DafnyType + Eq + Hash, T17: DafnyType + Eq + Hash, T18: DafnyType + Eq + Hash, T19: DafnyType + Eq + Hash> Eq
3945        for Tuple20<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15, T16, T17, T18, T19> {}
3946
3947    impl<T0: DafnyType + Hash, T1: DafnyType + Hash, T2: DafnyType + Hash, T3: DafnyType + Hash, T4: DafnyType + Hash, T5: DafnyType + Hash, T6: DafnyType + Hash, T7: DafnyType + Hash, T8: DafnyType + Hash, T9: DafnyType + Hash, T10: DafnyType + Hash, T11: DafnyType + Hash, T12: DafnyType + Hash, T13: DafnyType + Hash, T14: DafnyType + Hash, T15: DafnyType + Hash, T16: DafnyType + Hash, T17: DafnyType + Hash, T18: DafnyType + Hash, T19: DafnyType + Hash> Hash
3948        for Tuple20<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15, T16, T17, T18, T19> {
3949        fn hash<_H: Hasher>(&self, _state: &mut _H) {
3950            match self {
3951                Tuple20::_T20{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, _19, } => {
3952                    Hash::hash(_0, _state);
3953                    Hash::hash(_1, _state);
3954                    Hash::hash(_2, _state);
3955                    Hash::hash(_3, _state);
3956                    Hash::hash(_4, _state);
3957                    Hash::hash(_5, _state);
3958                    Hash::hash(_6, _state);
3959                    Hash::hash(_7, _state);
3960                    Hash::hash(_8, _state);
3961                    Hash::hash(_9, _state);
3962                    Hash::hash(_10, _state);
3963                    Hash::hash(_11, _state);
3964                    Hash::hash(_12, _state);
3965                    Hash::hash(_13, _state);
3966                    Hash::hash(_14, _state);
3967                    Hash::hash(_15, _state);
3968                    Hash::hash(_16, _state);
3969                    Hash::hash(_17, _state);
3970                    Hash::hash(_18, _state);
3971                    Hash::hash(_19, _state)
3972                },
3973            }
3974        }
3975    }
3976
3977    impl<T0: DafnyType, T1: DafnyType, T2: DafnyType, T3: DafnyType, T4: DafnyType, T5: DafnyType, T6: DafnyType, T7: DafnyType, T8: DafnyType, T9: DafnyType, T10: DafnyType, T11: DafnyType, T12: DafnyType, T13: DafnyType, T14: DafnyType, T15: DafnyType, T16: DafnyType, T17: DafnyType, T18: DafnyType, T19: DafnyType> AsRef<Tuple20<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15, T16, T17, T18, T19>>
3978        for Tuple20<T0, T1, T2, T3, T4, T5, T6, T7, T8, T9, T10, T11, T12, T13, T14, T15, T16, T17, T18, T19> {
3979        fn as_ref(&self) -> &Self {
3980            self
3981        }
3982    }
3983}
dafny_runtime/system/mod.rs

dafny_runtime/system/
mod.rs
