creusot_std/std/
ops.rs

1use crate::prelude::*;
2#[cfg(creusot)]
3use core::convert::Infallible;
4#[cfg(feature = "nightly")]
5use core::marker::Tuple;
6use core::ops::*;
7
8// Note: we should NOT give a generic extern spec for Deref::deref, since this
9// method is an exception being used both as a logic function and as a program
10// function. See #1235.
11
12/// `FnOnceExt` is an extension trait for the `FnOnce` trait, used for
13/// adding a specification to closures. It should not be used directly.
14#[cfg(feature = "nightly")]
15pub trait FnOnceExt<Args: Tuple> {
16    type Output;
17
18    #[logic(prophetic)]
19    fn precondition(self, a: Args) -> bool;
20
21    #[logic(prophetic)]
22    fn postcondition_once(self, a: Args, res: Self::Output) -> bool;
23}
24
25#[cfg(not(feature = "nightly"))]
26pub trait FnOnceExt<Args> {
27    type Output;
28}
29
30/// `FnMutExt` is an extension trait for the `FnMut` trait, used for
31/// adding a specification to closures. It should not be used directly.
32#[cfg(feature = "nightly")]
33pub trait FnMutExt<Args: Tuple>: FnOnceExt<Args> {
34    #[logic(prophetic)]
35    fn postcondition_mut(self, _: Args, _: Self, _: Self::Output) -> bool;
36
37    #[logic(prophetic)]
38    fn hist_inv(self, _: Self) -> bool;
39
40    #[logic(law)]
41    #[requires(self.postcondition_mut(args, res_state, res))]
42    #[ensures(self.hist_inv(res_state))]
43    fn postcondition_mut_hist_inv(self, args: Args, res_state: Self, res: Self::Output);
44
45    #[logic(law)]
46    #[ensures(self.hist_inv(self))]
47    fn hist_inv_refl(self);
48
49    #[logic(law)]
50    #[requires(self.hist_inv(b))]
51    #[requires(b.hist_inv(c))]
52    #[ensures(self.hist_inv(c))]
53    fn hist_inv_trans(self, b: Self, c: Self);
54
55    #[logic(law)]
56    #[ensures(self.postcondition_once(args, res) ==
57              exists<res_state: Self> self.postcondition_mut(args, res_state, res) && resolve(res_state))]
58    fn fn_mut_once(self, args: Args, res: Self::Output);
59}
60
61#[cfg(not(feature = "nightly"))]
62pub trait FnMutExt<Args>: FnOnceExt<Args> {}
63
64/// `FnExt` is an extension trait for the `Fn` trait, used for
65/// adding a specification to closures. It should not be used directly.
66#[cfg(feature = "nightly")]
67pub trait FnExt<Args: Tuple>: FnMutExt<Args> {
68    #[logic(prophetic)]
69    fn postcondition(self, _: Args, _: Self::Output) -> bool;
70
71    #[logic(law)]
72    #[ensures(self.postcondition_mut(args, res_state, res) == (self.postcondition(args, res) && self == res_state))]
73    fn fn_mut(self, args: Args, res_state: Self, res: Self::Output);
74
75    #[logic(law)]
76    #[ensures(self.postcondition_once(args, res) == (self.postcondition(args, res) && resolve(self)))]
77    fn fn_once(self, args: Args, res: Self::Output);
78
79    #[logic(law)]
80    #[ensures(self.hist_inv(res_state) == (self == res_state))]
81    fn fn_hist_inv(self, res_state: Self);
82}
83
84/// `FnExt` is an extension trait for the `Fn` trait, used for
85/// adding a specification to closures. It should not be used directly.
86#[cfg(not(feature = "nightly"))]
87pub trait FnExt<Args>: FnMutExt<Args> {}
88
89#[cfg(feature = "nightly")]
90impl<Args: Tuple, F: ?Sized + FnOnce<Args>> FnOnceExt<Args> for F {
91    type Output = <Self as FnOnce<Args>>::Output;
92
93    #[logic(open, prophetic, inline)]
94    #[allow(unused_variables)]
95    #[intrinsic("precondition")]
96    fn precondition(self, args: Args) -> bool {
97        dead
98    }
99
100    #[logic(open, prophetic, inline)]
101    #[allow(unused_variables)]
102    #[intrinsic("postcondition_once")]
103    fn postcondition_once(self, args: Args, result: Self::Output) -> bool {
104        dead
105    }
106}
107
108#[cfg(feature = "nightly")]
109impl<Args: Tuple, F: ?Sized + FnMut<Args>> FnMutExt<Args> for F {
110    #[logic(open, prophetic, inline)]
111    #[allow(unused_variables)]
112    #[intrinsic("postcondition_mut")]
113    fn postcondition_mut(self, args: Args, result_state: Self, result: Self::Output) -> bool {
114        dead
115    }
116
117    #[logic(open, prophetic, inline)]
118    #[allow(unused_variables)]
119    #[intrinsic("hist_inv")]
120    fn hist_inv(self, result_state: Self) -> bool {
121        dead
122    }
123
124    #[trusted]
125    #[logic(law)]
126    #[requires(self.postcondition_mut(args, res_state, res))]
127    #[ensures(self.hist_inv(res_state))]
128    fn postcondition_mut_hist_inv(self, args: Args, res_state: Self, res: Self::Output) {}
129
130    #[trusted]
131    #[logic(law)]
132    #[ensures(self.hist_inv(self))]
133    fn hist_inv_refl(self) {}
134
135    #[trusted]
136    #[logic(law)]
137    #[requires(self.hist_inv(b))]
138    #[requires(b.hist_inv(c))]
139    #[ensures(self.hist_inv(c))]
140    fn hist_inv_trans(self, b: Self, c: Self) {}
141
142    #[logic(law)]
143    #[trusted]
144    #[ensures(self.postcondition_once(args, res) ==
145              exists<res_state: Self> self.postcondition_mut(args, res_state, res) && resolve(res_state))]
146    fn fn_mut_once(self, args: Args, res: Self::Output) {}
147}
148
149#[cfg(feature = "nightly")]
150impl<Args: Tuple, F: ?Sized + Fn<Args>> FnExt<Args> for F {
151    #[logic(open, inline)]
152    #[allow(unused_variables)]
153    #[intrinsic("postcondition")]
154    fn postcondition(self, args: Args, result: Self::Output) -> bool {
155        dead
156    }
157
158    #[logic(law)]
159    #[trusted]
160    #[ensures(self.postcondition_mut(args, res_state, res) == (self.postcondition(args, res) && self == res_state))]
161    fn fn_mut(self, args: Args, res_state: Self, res: Self::Output) {}
162
163    #[logic(law)]
164    #[trusted]
165    #[ensures(self.postcondition_once(args, res) == (self.postcondition(args, res) && resolve(self)))]
166    fn fn_once(self, args: Args, res: Self::Output) {}
167
168    #[logic(law)]
169    #[trusted]
170    #[ensures(self.hist_inv(res_state) == (self == res_state))]
171    fn fn_hist_inv(self, res_state: Self) {}
172}
173
174extern_spec! {
175    mod core {
176        mod ops {
177            trait FnOnce<Args> where Args: Tuple {
178                #[requires(self.precondition(arg))]
179                #[ensures(self.postcondition_once(arg, result))]
180                fn call_once(self, arg: Args) -> Self::Output;
181            }
182
183            trait FnMut<Args> where Args: Tuple {
184                #[requires((*self).precondition(arg))]
185                #[ensures((*self).postcondition_mut(arg, ^self, result))]
186                fn call_mut(&mut self, arg: Args) -> Self::Output;
187            }
188
189            trait Fn<Args> where Args: Tuple {
190                #[requires((*self).precondition(arg))]
191                #[ensures((*self).postcondition(arg, result))]
192                fn call(&self, arg: Args) -> Self::Output;
193            }
194
195            trait Deref {
196                #[check(ghost)]
197                #[requires(false)]
198                fn deref(&self) -> &Self::Target;
199            }
200
201            trait DerefMut {
202                #[check(ghost)]
203                #[requires(false)]
204                fn deref_mut(&mut self) -> &mut Self::Target;
205            }
206        }
207    }
208}
209
210impl<T: DeepModel> DeepModel for Bound<T> {
211    type DeepModelTy = Bound<T::DeepModelTy>;
212
213    #[logic(open)]
214    fn deep_model(self) -> Self::DeepModelTy {
215        match self {
216            Bound::Included(b) => Bound::Included(b.deep_model()),
217            Bound::Excluded(b) => Bound::Excluded(b.deep_model()),
218            Bound::Unbounded => Bound::Unbounded,
219        }
220    }
221}
222
223/// Methods for the specification of [`std::ops::RangeBounds`].
224pub trait RangeBounds<T: ?Sized + DeepModel<DeepModelTy: OrdLogic>>:
225    core::ops::RangeBounds<T>
226{
227    #[logic]
228    fn start_bound_logic(&self) -> Bound<&T>;
229
230    #[logic]
231    fn end_bound_logic(&self) -> Bound<&T>;
232}
233
234/// Membership to an interval `(Bound<T>, Bound<T>)`.
235#[logic(open)]
236pub fn between<T: OrdLogic>(lo: Bound<T>, item: T, hi: Bound<T>) -> bool {
237    lower_bound(lo, item) && upper_bound(item, hi)
238}
239
240/// Comparison with a lower bound.
241#[logic(open)]
242pub fn lower_bound<T: OrdLogic>(lo: Bound<T>, item: T) -> bool {
243    pearlite! {
244        match lo {
245            Bound::Included(lo) => lo <= item,
246            Bound::Excluded(lo) => lo < item,
247            Bound::Unbounded => true,
248        }
249    }
250}
251
252/// Comparison with an upper bound.
253#[logic(open)]
254pub fn upper_bound<T: OrdLogic>(item: T, hi: Bound<T>) -> bool {
255    pearlite! {
256        match hi {
257            Bound::Included(hi) => item <= hi,
258            Bound::Excluded(lo) => lo < item,
259            Bound::Unbounded => true,
260        }
261    }
262}
263
264extern_spec! {
265    mod core {
266        mod ops {
267            trait RangeBounds<T>
268            where
269                Self: RangeBounds<T>,
270                T: ?Sized + DeepModel,
271                T::DeepModelTy: OrdLogic,
272            {
273                #[ensures(result == self.start_bound_logic())]
274                fn start_bound(&self) -> Bound<&T>;
275
276                #[ensures(result == self.end_bound_logic())]
277                fn end_bound(&self) -> Bound<&T>;
278
279                #[ensures(result == between(self.start_bound_logic().deep_model(), item.deep_model(), self.end_bound_logic().deep_model()))]
280                fn contains<U>(&self, item: &U) -> bool
281                where
282                    T: PartialOrd<U>,
283                    U: ?Sized + PartialOrd<T> + DeepModel<DeepModelTy = T::DeepModelTy>;
284
285                #[ensures(result == !exists<item: T::DeepModelTy> between(self.start_bound_logic().deep_model(), item, self.end_bound_logic().deep_model()))]
286                fn is_empty(&self) -> bool
287                where T: PartialOrd;
288            }
289        }
290    }
291
292    impl<T: Copy> Bound<&T> {
293        #[erasure]
294        #[ensures(result == match self {
295            Bound::Unbounded => Bound::Unbounded,
296            Bound::Included(x) => Bound::Included(*x),
297            Bound::Excluded(x) => Bound::Excluded(*x),
298        })]
299        fn copied(self) -> Bound<T> {
300            match self {
301                Bound::Unbounded => Bound::Unbounded,
302                Bound::Included(x) => Bound::Included(*x),
303                Bound::Excluded(x) => Bound::Excluded(*x),
304            }
305        }
306    }
307}
308
309impl<T: DeepModel<DeepModelTy: OrdLogic>> RangeBounds<T> for RangeFull {
310    #[logic(open)]
311    fn start_bound_logic(&self) -> Bound<&T> {
312        Bound::Unbounded
313    }
314
315    #[logic(open)]
316    fn end_bound_logic(&self) -> Bound<&T> {
317        Bound::Unbounded
318    }
319}
320
321impl<T: DeepModel<DeepModelTy: OrdLogic>> RangeBounds<T> for RangeFrom<T> {
322    #[logic(open)]
323    fn start_bound_logic(&self) -> Bound<&T> {
324        Bound::Included(&self.start)
325    }
326
327    #[logic(open)]
328    fn end_bound_logic(&self) -> Bound<&T> {
329        Bound::Unbounded
330    }
331}
332
333impl<T: DeepModel<DeepModelTy: OrdLogic>> RangeBounds<T> for RangeTo<T> {
334    #[logic(open)]
335    fn start_bound_logic(&self) -> Bound<&T> {
336        Bound::Unbounded
337    }
338
339    #[logic(open)]
340    fn end_bound_logic(&self) -> Bound<&T> {
341        Bound::Excluded(&self.end)
342    }
343}
344
345impl<T: DeepModel<DeepModelTy: OrdLogic>> RangeBounds<T> for Range<T> {
346    #[logic(open)]
347    fn start_bound_logic(&self) -> Bound<&T> {
348        Bound::Included(&self.start)
349    }
350
351    #[logic(open)]
352    fn end_bound_logic(&self) -> Bound<&T> {
353        Bound::Excluded(&self.end)
354    }
355}
356
357impl<T: DeepModel<DeepModelTy: OrdLogic>> RangeBounds<T> for RangeInclusive<T> {
358    #[logic(open)]
359    fn start_bound_logic(&self) -> Bound<&T> {
360        Bound::Included(&self.start_log())
361    }
362
363    #[logic(opaque)]
364    fn end_bound_logic(&self) -> Bound<&T> {
365        dead
366    }
367}
368
369impl<T: DeepModel<DeepModelTy: OrdLogic>> RangeBounds<T> for RangeToInclusive<T> {
370    #[logic(open)]
371    fn start_bound_logic(&self) -> Bound<&T> {
372        Bound::Unbounded
373    }
374
375    #[logic(open)]
376    fn end_bound_logic(&self) -> Bound<&T> {
377        Bound::Included(&self.end)
378    }
379}
380
381impl<T: DeepModel<DeepModelTy: OrdLogic>> RangeBounds<T> for (Bound<T>, Bound<T>) {
382    #[logic(open)]
383    fn start_bound_logic(&self) -> Bound<&T> {
384        match *self {
385            (Bound::Included(ref start), _) => Bound::Included(start),
386            (Bound::Excluded(ref start), _) => Bound::Excluded(start),
387            (Bound::Unbounded, _) => Bound::Unbounded,
388        }
389    }
390
391    #[logic(open)]
392    fn end_bound_logic(&self) -> Bound<&T> {
393        match *self {
394            (_, Bound::Included(ref end)) => Bound::Included(end),
395            (_, Bound::Excluded(ref end)) => Bound::Excluded(end),
396            (_, Bound::Unbounded) => Bound::Unbounded,
397        }
398    }
399}
400
401impl<'a, T: ?Sized + 'a + DeepModel<DeepModelTy: OrdLogic>> RangeBounds<T>
402    for (Bound<&'a T>, Bound<&'a T>)
403{
404    #[logic(open)]
405    fn start_bound_logic(&self) -> Bound<&T> {
406        self.0
407    }
408
409    #[logic(open)]
410    fn end_bound_logic(&self) -> Bound<&T> {
411        self.1
412    }
413}
414
415impl<T: DeepModel<DeepModelTy: OrdLogic>> RangeBounds<T> for RangeFrom<&T> {
416    #[logic(open)]
417    fn start_bound_logic(&self) -> Bound<&T> {
418        Bound::Included(self.start)
419    }
420
421    #[logic(open)]
422    fn end_bound_logic(&self) -> Bound<&T> {
423        Bound::Unbounded
424    }
425}
426
427impl<T: DeepModel<DeepModelTy: OrdLogic>> RangeBounds<T> for RangeTo<&T> {
428    #[logic(open)]
429    fn start_bound_logic(&self) -> Bound<&T> {
430        Bound::Unbounded
431    }
432
433    #[logic(open)]
434    fn end_bound_logic(&self) -> Bound<&T> {
435        Bound::Excluded(self.end)
436    }
437}
438
439impl<T: DeepModel<DeepModelTy: OrdLogic>> RangeBounds<T> for Range<&T> {
440    #[logic(open)]
441    fn start_bound_logic(&self) -> Bound<&T> {
442        Bound::Included(self.start)
443    }
444
445    #[logic(open)]
446    fn end_bound_logic(&self) -> Bound<&T> {
447        Bound::Excluded(self.end)
448    }
449}
450
451// I don't know why this impl is different from the one for `RangeInclusive<T>`.
452impl<T: DeepModel<DeepModelTy: OrdLogic>> RangeBounds<T> for RangeInclusive<&T> {
453    #[logic(open)]
454    fn start_bound_logic(&self) -> Bound<&T> {
455        Bound::Included(&self.start_log())
456    }
457
458    #[logic(open)]
459    fn end_bound_logic(&self) -> Bound<&T> {
460        Bound::Included(&self.end_log())
461    }
462}
463
464impl<T: DeepModel<DeepModelTy: OrdLogic>> RangeBounds<T> for RangeToInclusive<&T> {
465    #[logic(open)]
466    fn start_bound_logic(&self) -> Bound<&T> {
467        Bound::Unbounded
468    }
469
470    #[logic(open)]
471    fn end_bound_logic(&self) -> Bound<&T> {
472        Bound::Included(self.end)
473    }
474}
475
476#[cfg(feature = "nightly")]
477impl<T: DeepModel<DeepModelTy: OrdLogic>> RangeBounds<T> for core::range::Range<T> {
478    #[logic(open)]
479    fn start_bound_logic(&self) -> Bound<&T> {
480        Bound::Included(&self.start)
481    }
482
483    #[logic(open)]
484    fn end_bound_logic(&self) -> Bound<&T> {
485        Bound::Excluded(&self.end)
486    }
487}
488
489#[cfg(feature = "nightly")]
490impl<T: DeepModel<DeepModelTy: OrdLogic>> RangeBounds<T> for core::range::Range<&T> {
491    #[logic(open)]
492    fn start_bound_logic(&self) -> Bound<&T> {
493        Bound::Included(self.start)
494    }
495
496    #[logic(open)]
497    fn end_bound_logic(&self) -> Bound<&T> {
498        Bound::Excluded(self.end)
499    }
500}
501
502#[cfg(feature = "nightly")]
503impl<T: DeepModel<DeepModelTy: OrdLogic>> RangeBounds<T> for core::range::RangeFrom<T> {
504    #[logic(open)]
505    fn start_bound_logic(&self) -> Bound<&T> {
506        Bound::Included(&self.start)
507    }
508
509    #[logic(open)]
510    fn end_bound_logic(&self) -> Bound<&T> {
511        Bound::Unbounded
512    }
513}
514
515#[cfg(feature = "nightly")]
516impl<T: DeepModel<DeepModelTy: OrdLogic>> RangeBounds<T> for core::range::RangeFrom<&T> {
517    #[logic(open)]
518    fn start_bound_logic(&self) -> Bound<&T> {
519        Bound::Included(self.start)
520    }
521
522    #[logic(open)]
523    fn end_bound_logic(&self) -> Bound<&T> {
524        Bound::Unbounded
525    }
526}
527
528#[cfg(feature = "nightly")]
529impl<T: DeepModel<DeepModelTy: OrdLogic>> RangeBounds<T> for core::range::RangeInclusive<T> {
530    #[logic(open)]
531    fn start_bound_logic(&self) -> Bound<&T> {
532        Bound::Included(&self.start)
533    }
534
535    #[logic(open)]
536    fn end_bound_logic(&self) -> Bound<&T> {
537        Bound::Included(&self.last)
538    }
539}
540
541#[cfg(feature = "nightly")]
542impl<T: DeepModel<DeepModelTy: OrdLogic>> RangeBounds<T> for core::range::RangeInclusive<&T> {
543    #[logic(open)]
544    fn start_bound_logic(&self) -> Bound<&T> {
545        Bound::Included(self.start)
546    }
547
548    #[logic(open)]
549    fn end_bound_logic(&self) -> Bound<&T> {
550        Bound::Included(self.last)
551    }
552}
553
554pub trait RangeInclusiveExt<Idx> {
555    #[logic]
556    fn new_log(start: Idx, end: Idx) -> Self;
557
558    #[logic]
559    fn start_log(self) -> Idx;
560
561    #[logic]
562    fn end_log(self) -> Idx;
563
564    #[logic]
565    fn is_empty_log(self) -> bool
566    where
567        Idx: DeepModel,
568        Idx::DeepModelTy: OrdLogic;
569}
570
571impl<Idx> RangeInclusiveExt<Idx> for RangeInclusive<Idx> {
572    #[logic(opaque)]
573    #[trusted]
574    #[ensures(start == result.start_log() && end == result.end_log())]
575    fn new_log(start: Idx, end: Idx) -> Self {
576        dead
577    }
578
579    #[logic(opaque)]
580    fn start_log(self) -> Idx {
581        dead
582    }
583
584    #[logic(opaque)]
585    fn end_log(self) -> Idx {
586        dead
587    }
588
589    #[logic(opaque)]
590    #[trusted]
591    #[ensures(!result ==> self.start_log().deep_model() <= self.end_log().deep_model())]
592    fn is_empty_log(self) -> bool
593    where
594        Idx: DeepModel,
595        Idx::DeepModelTy: OrdLogic,
596    {
597        dead
598    }
599}
600
601extern_spec! {
602    impl<Idx> RangeInclusive<Idx> {
603        #[ensures(result.start_log() == start)]
604        #[ensures(result.end_log() == end)]
605        #[ensures(start.deep_model() <= end.deep_model() ==> !result.is_empty_log())]
606        fn new(start: Idx, end: Idx) -> Self
607            where Idx: DeepModel, Idx::DeepModelTy: OrdLogic;
608
609        #[ensures(*result == self.start_log())]
610        fn start(&self) -> &Idx;
611
612        #[ensures(*result == self.end_log())]
613        fn end(&self) -> &Idx;
614    }
615
616    impl<Idx: PartialOrd<Idx> + DeepModel> RangeInclusive<Idx>
617    where Idx::DeepModelTy: OrdLogic
618    {
619        #[ensures(result == self.is_empty_log())]
620        fn is_empty(&self) -> bool;
621    }
622}
623
624extern_spec! {
625    impl<T> Try for Option<T> {
626        #[ensures(result == Some(output))]
627        fn from_output(output: T) -> Self {
628            Some(output)
629        }
630
631        #[ensures(match self {
632            Some(v) => result == ControlFlow::Continue(v),
633            None => result == ControlFlow::Break(None)
634        })]
635        fn branch(self) -> ControlFlow<Option<Infallible>, T> {
636            match self {
637                Some(v) => ControlFlow::Continue(v),
638                None => ControlFlow::Break(None),
639            }
640        }
641    }
642
643    impl<T> FromResidual<Option<Infallible>> for Option<T> {
644        #[ensures(result == None)]
645        fn from_residual(residual: Option<Infallible>) -> Self {
646            match residual {
647                None => None,
648            }
649        }
650    }
651
652    impl<T, E> Try for Result<T, E> {
653        #[ensures(result == Ok(output))]
654        fn from_output(output: T) -> Self {
655            Ok(output)
656        }
657
658        #[ensures(match self {
659            Ok(v) => result == ControlFlow::Continue(v),
660            Err(e) => result == ControlFlow::Break(Err(e))
661        })]
662        fn branch(self) -> ControlFlow<Result<Infallible, E>, T> {
663            match self {
664                Ok(v) => ControlFlow::Continue(v),
665                Err(e) => ControlFlow::Break(Err(e)),
666            }
667        }
668    }
669
670    impl<T, E, F: From<E>> FromResidual<Result<Infallible, E>> for Result<T, F> {
671        #[ensures(match (result, residual) {
672            (Err(result), Err(residual)) => F::from.postcondition((residual,), result),
673            _ => false,
674        })]
675        fn from_residual(residual: Result<Infallible, E>) -> Self {
676            match residual {
677                Err(e) => Err(core::convert::From::from(e)),
678            }
679        }
680    }
681}
682
683/// Dummy impls that don't use the unstable traits Tuple, FnOnce<Args>, FnMut<Args>, Fn<Args>
684#[cfg(not(feature = "nightly"))]
685mod impls {
686    use crate::std::ops::*;
687
688    impl<O, F: FnOnce() -> O> FnOnceExt<()> for F {
689        type Output = O;
690    }
691    impl<O, F: FnMut() -> O> FnMutExt<()> for F {}
692    impl<O, F: Fn() -> O> FnExt<()> for F {}
693
694    macro_rules! impl_fn {
695        ( $( $tuple:tt ),+ ) => {
696            impl<$($tuple),+, O, F: FnOnce($($tuple),+) -> O> FnOnceExt<($($tuple),+,)> for F {
697                type Output = O;
698            }
699            impl<$($tuple),+, O, F: FnMut($($tuple),+) -> O> FnMutExt<($($tuple),+,)> for F {}
700            impl<$($tuple),+, O, F: Fn($($tuple),+) -> O> FnExt<($($tuple),+,)> for F {}
701        };
702    }
703
704    impl_fn! { A1 }
705    impl_fn! { A1, A2 }
706    impl_fn! { A1, A2, A3 }
707    impl_fn! { A1, A2, A3, A4 }
708    impl_fn! { A1, A2, A3, A4, A5 }
709    impl_fn! { A1, A2, A3, A4, A5, A6 }
710    impl_fn! { A1, A2, A3, A4, A5, A6, A7 }
711    impl_fn! { A1, A2, A3, A4, A5, A6, A7, A8 }
712    impl_fn! { A1, A2, A3, A4, A5, A6, A7, A8, A9 }
713}
creusot_std/std/ops.rs

creusot_std/std/
ops.rs
