diff options
Diffstat (limited to 'tests')
20 files changed, 5085 insertions, 26 deletions
diff --git a/tests/ui/asm/fail-const-eval-issue-121099.rs b/tests/ui/asm/fail-const-eval-issue-121099.rs new file mode 100644 index 00000000000..bed6fc9b39f --- /dev/null +++ b/tests/ui/asm/fail-const-eval-issue-121099.rs @@ -0,0 +1,11 @@ +//@ build-fail +//@ needs-asm-support +#![feature(asm_const)] + +use std::arch::global_asm; + +fn main() {} + +global_asm!("/* {} */", const 1 << 500); //~ ERROR evaluation of constant value failed [E0080] + +global_asm!("/* {} */", const 1 / 0); //~ ERROR evaluation of constant value failed [E0080] diff --git a/tests/ui/asm/fail-const-eval-issue-121099.stderr b/tests/ui/asm/fail-const-eval-issue-121099.stderr new file mode 100644 index 00000000000..51d283218d2 --- /dev/null +++ b/tests/ui/asm/fail-const-eval-issue-121099.stderr @@ -0,0 +1,15 @@ +error[E0080]: evaluation of constant value failed + --> $DIR/fail-const-eval-issue-121099.rs:9:31 + | +LL | global_asm!("/* {} */", const 1 << 500); + | ^^^^^^^^ attempt to shift left by `500_i32`, which would overflow + +error[E0080]: evaluation of constant value failed + --> $DIR/fail-const-eval-issue-121099.rs:11:31 + | +LL | global_asm!("/* {} */", const 1 / 0); + | ^^^^^ attempt to divide `1_i32` by zero + +error: aborting due to 2 previous errors + +For more information about this error, try `rustc --explain E0080`. diff --git a/tests/ui/cast/unsized-union-ice.rs b/tests/ui/cast/unsized-union-ice.rs new file mode 100644 index 00000000000..11aefe57f1d --- /dev/null +++ b/tests/ui/cast/unsized-union-ice.rs @@ -0,0 +1,14 @@ +// Regression test for https://github.com/rust-lang/rust/issues/122581 +// This used to ICE, because the union was unsized and the pointer casting code +// assumed that non-struct ADTs must be sized. + +union Union { + val: std::mem::ManuallyDrop<[u8]>, + //~^ ERROR the size for values of type `[u8]` cannot be known at compilation time +} + +fn cast(ptr: *const ()) -> *const Union { + ptr as _ +} + +fn main() {} diff --git a/tests/ui/cast/unsized-union-ice.stderr b/tests/ui/cast/unsized-union-ice.stderr new file mode 100644 index 00000000000..05f86457829 --- /dev/null +++ b/tests/ui/cast/unsized-union-ice.stderr @@ -0,0 +1,23 @@ +error[E0277]: the size for values of type `[u8]` cannot be known at compilation time + --> $DIR/unsized-union-ice.rs:6:10 + | +LL | val: std::mem::ManuallyDrop<[u8]>, + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ doesn't have a size known at compile-time + | + = help: within `ManuallyDrop<[u8]>`, the trait `Sized` is not implemented for `[u8]`, which is required by `ManuallyDrop<[u8]>: Sized` +note: required because it appears within the type `ManuallyDrop<[u8]>` + --> $SRC_DIR/core/src/mem/manually_drop.rs:LL:COL + = note: no field of a union may have a dynamically sized type + = help: change the field's type to have a statically known size +help: borrowed types always have a statically known size + | +LL | val: &std::mem::ManuallyDrop<[u8]>, + | + +help: the `Box` type always has a statically known size and allocates its contents in the heap + | +LL | val: Box<std::mem::ManuallyDrop<[u8]>>, + | ++++ + + +error: aborting due to 1 previous error + +For more information about this error, try `rustc --explain E0277`. diff --git a/tests/ui/compiletest-self-test/auxiliary/print-it-works.rs b/tests/ui/compiletest-self-test/auxiliary/print-it-works.rs new file mode 100644 index 00000000000..09411eb121c --- /dev/null +++ b/tests/ui/compiletest-self-test/auxiliary/print-it-works.rs @@ -0,0 +1,3 @@ +fn main() { + println!("it works"); +} diff --git a/tests/ui/compiletest-self-test/test-aux-bin.rs b/tests/ui/compiletest-self-test/test-aux-bin.rs new file mode 100644 index 00000000000..9e01e3ffabf --- /dev/null +++ b/tests/ui/compiletest-self-test/test-aux-bin.rs @@ -0,0 +1,9 @@ +//@ ignore-cross-compile because we run the compiled code +//@ aux-bin: print-it-works.rs +//@ run-pass + +fn main() { + let stdout = + std::process::Command::new("auxiliary/bin/print-it-works").output().unwrap().stdout; + assert_eq!(stdout, b"it works\n"); +} diff --git a/tests/ui/fmt/format-args-non-identifier-diagnostics.fixed b/tests/ui/fmt/format-args-non-identifier-diagnostics.fixed new file mode 100644 index 00000000000..bd4db948067 --- /dev/null +++ b/tests/ui/fmt/format-args-non-identifier-diagnostics.fixed @@ -0,0 +1,10 @@ +// Checks that there is a suggestion for simple tuple index access expression (used where an +// identifier is expected in a format arg) to use positional arg instead. +// Issue: <https://github.com/rust-lang/rust/issues/122535>. +//@ run-rustfix + +fn main() { + let x = (1,); + println!("{0}", x.0); + //~^ ERROR invalid format string +} diff --git a/tests/ui/fmt/format-args-non-identifier-diagnostics.rs b/tests/ui/fmt/format-args-non-identifier-diagnostics.rs new file mode 100644 index 00000000000..aab705341f7 --- /dev/null +++ b/tests/ui/fmt/format-args-non-identifier-diagnostics.rs @@ -0,0 +1,10 @@ +// Checks that there is a suggestion for simple tuple index access expression (used where an +// identifier is expected in a format arg) to use positional arg instead. +// Issue: <https://github.com/rust-lang/rust/issues/122535>. +//@ run-rustfix + +fn main() { + let x = (1,); + println!("{x.0}"); + //~^ ERROR invalid format string +} diff --git a/tests/ui/fmt/format-args-non-identifier-diagnostics.stderr b/tests/ui/fmt/format-args-non-identifier-diagnostics.stderr new file mode 100644 index 00000000000..08abba2854e --- /dev/null +++ b/tests/ui/fmt/format-args-non-identifier-diagnostics.stderr @@ -0,0 +1,13 @@ +error: invalid format string: tuple index access isn't supported + --> $DIR/format-args-non-identifier-diagnostics.rs:8:16 + | +LL | println!("{x.0}"); + | ^^^ not supported in format string + | +help: consider using a positional formatting argument instead + | +LL | println!("{0}", x.0); + | ~ +++++ + +error: aborting due to 1 previous error + diff --git a/tests/ui/lint/lint-qualification.fixed b/tests/ui/lint/lint-qualification.fixed index 6fe6ba2792f..2070bbcef52 100644 --- a/tests/ui/lint/lint-qualification.fixed +++ b/tests/ui/lint/lint-qualification.fixed @@ -16,7 +16,6 @@ fn main() { let _ = || -> Result<(), ()> { try!(Ok(())); Ok(()) }; // issue #37345 let _ = String::new(); //~ ERROR: unnecessary qualification - let _ = std::env::current_dir(); //~ ERROR: unnecessary qualification let _: Vec<String> = Vec::<String>::new(); //~^ ERROR: unnecessary qualification @@ -27,7 +26,7 @@ fn main() { let _: std::fmt::Result = Ok(()); // don't report unnecessary qualification because fix(#122373) for issue #121331 - let _ = <bool as Default>::default(); // issue #121999 + let _ = <bool as Default>::default(); // issue #121999 (modified) //~^ ERROR: unnecessary qualification macro_rules! m { ($a:ident, $b:ident) => { diff --git a/tests/ui/lint/lint-qualification.rs b/tests/ui/lint/lint-qualification.rs index 19d339b006c..41b7e17c6ed 100644 --- a/tests/ui/lint/lint-qualification.rs +++ b/tests/ui/lint/lint-qualification.rs @@ -16,7 +16,6 @@ fn main() { let _ = || -> Result<(), ()> { try!(Ok(())); Ok(()) }; // issue #37345 let _ = std::string::String::new(); //~ ERROR: unnecessary qualification - let _ = ::std::env::current_dir(); //~ ERROR: unnecessary qualification let _: std::vec::Vec<String> = std::vec::Vec::<String>::new(); //~^ ERROR: unnecessary qualification @@ -27,7 +26,7 @@ fn main() { let _: std::fmt::Result = Ok(()); // don't report unnecessary qualification because fix(#122373) for issue #121331 - let _ = <bool as ::std::default::Default>::default(); // issue #121999 + let _ = <bool as std::default::Default>::default(); // issue #121999 (modified) //~^ ERROR: unnecessary qualification macro_rules! m { ($a:ident, $b:ident) => { diff --git a/tests/ui/lint/lint-qualification.stderr b/tests/ui/lint/lint-qualification.stderr index 9e5c9b2df13..cefa54a12ae 100644 --- a/tests/ui/lint/lint-qualification.stderr +++ b/tests/ui/lint/lint-qualification.stderr @@ -40,19 +40,7 @@ LL + let _ = String::new(); | error: unnecessary qualification - --> $DIR/lint-qualification.rs:19:13 - | -LL | let _ = ::std::env::current_dir(); - | ^^^^^^^^^^^^^^^^^^^^^^^ - | -help: remove the unnecessary path segments - | -LL - let _ = ::std::env::current_dir(); -LL + let _ = std::env::current_dir(); - | - -error: unnecessary qualification - --> $DIR/lint-qualification.rs:21:12 + --> $DIR/lint-qualification.rs:20:12 | LL | let _: std::vec::Vec<String> = std::vec::Vec::<String>::new(); | ^^^^^^^^^^^^^^^^^^^^^ @@ -64,7 +52,7 @@ LL + let _: Vec<String> = std::vec::Vec::<String>::new(); | error: unnecessary qualification - --> $DIR/lint-qualification.rs:21:36 + --> $DIR/lint-qualification.rs:20:36 | LL | let _: std::vec::Vec<String> = std::vec::Vec::<String>::new(); | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ @@ -76,7 +64,7 @@ LL + let _: std::vec::Vec<String> = Vec::<String>::new(); | error: unused import: `std::fmt` - --> $DIR/lint-qualification.rs:25:9 + --> $DIR/lint-qualification.rs:24:9 | LL | use std::fmt; | ^^^^^^^^ @@ -88,16 +76,16 @@ LL | #![deny(unused_imports)] | ^^^^^^^^^^^^^^ error: unnecessary qualification - --> $DIR/lint-qualification.rs:30:13 + --> $DIR/lint-qualification.rs:29:13 | -LL | let _ = <bool as ::std::default::Default>::default(); // issue #121999 - | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +LL | let _ = <bool as std::default::Default>::default(); // issue #121999 (modified) + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ | help: remove the unnecessary path segments | -LL - let _ = <bool as ::std::default::Default>::default(); // issue #121999 -LL + let _ = <bool as Default>::default(); // issue #121999 +LL - let _ = <bool as std::default::Default>::default(); // issue #121999 (modified) +LL + let _ = <bool as Default>::default(); // issue #121999 (modified) | -error: aborting due to 8 previous errors +error: aborting due to 7 previous errors diff --git a/tests/ui/lint/unused-qualifications-global-paths.rs b/tests/ui/lint/unused-qualifications-global-paths.rs new file mode 100644 index 00000000000..8265c8a1694 --- /dev/null +++ b/tests/ui/lint/unused-qualifications-global-paths.rs @@ -0,0 +1,12 @@ +// Checks that `unused_qualifications` don't fire on explicit global paths. +// Issue: <https://github.com/rust-lang/rust/issues/122374>. + +//@ check-pass + +#![deny(unused_qualifications)] + +pub fn bar() -> u64 { + ::std::default::Default::default() +} + +fn main() {} diff --git a/tests/ui/parser/survive-peano-lesson-queue.rs b/tests/ui/parser/survive-peano-lesson-queue.rs new file mode 100644 index 00000000000..3608728594e --- /dev/null +++ b/tests/ui/parser/survive-peano-lesson-queue.rs @@ -0,0 +1,4907 @@ +//@ build-pass +// ignore-tidy-filelength +// ignore-tidy-linelength +// some very lightly modified generated code from issue rust-lang/rust#122715 +// the main differences are to strip the dependency on bumpalo so it can be tested separately +// the original purpose of this code was to implement a binomial queue, however it is extracted from Gallina +// which means that it uses an incredibly naive Peano representation of the natural numbers. +// this is fairly standard "someone did something very silly and we should try to gracefully handle it" + +#![allow(dead_code)] +#![allow(non_camel_case_types)] +#![allow(unused_imports)] +#![allow(non_snake_case)] +#![allow(unused_variables)] + +use std::marker::PhantomData; + +fn __nat_succ(x: u64) -> u64 { + x.checked_add(1).unwrap() +} + +macro_rules! __nat_elim { + ($zcase:expr, $pred:ident, $scase:expr, $val:expr) => { + { let v = $val; + if v == 0 { $zcase } else { let $pred = v - 1; $scase } } + } +} + +macro_rules! __andb { ($b1:expr, $b2:expr) => { $b1 && $b2 } } +macro_rules! __orb { ($b1:expr, $b2:expr) => { $b1 || $b2 } } + +fn __pos_onebit(x: u64) -> u64 { + x.checked_mul(2).unwrap() + 1 +} + +fn __pos_zerobit(x: u64) -> u64 { + x.checked_mul(2).unwrap() +} + +macro_rules! __pos_elim { + ($p:ident, $onebcase:expr, $p2:ident, $zerobcase:expr, $onecase:expr, $val:expr) => { + { + let n = $val; + if n == 1 { + $onecase + } else if (n & 1) == 0 { + let $p2 = n >> 1; + $zerobcase + } else { + let $p = n >> 1; + $onebcase + } + } + } +} + +fn __Z_frompos(z: u64) -> i64 { + use std::convert::TryFrom; + + i64::try_from(z).unwrap() +} + +fn __Z_fromneg(z : u64) -> i64 { + use std::convert::TryFrom; + + i64::try_from(z).unwrap().checked_neg().unwrap() +} + +macro_rules! __Z_elim { + ($zero_case:expr, $p:ident, $pos_case:expr, $p2:ident, $neg_case:expr, $val:expr) => { + { + let n = $val; + if n == 0 { + $zero_case + } else if n < 0 { + let $p2 = n.unsigned_abs(); + $neg_case + } else { + let $p = n as u64; + $pos_case + } + } + } +} + +fn __N_frompos(z: u64) -> u64 { + z +} + +macro_rules! __N_elim { + ($zero_case:expr, $p:ident, $pos_case:expr, $val:expr) => { + { let $p = $val; if $p == 0 { $zero_case } else { $pos_case } } + } +} + +type __pair<A, B> = (A, B); + +macro_rules! __pair_elim { + ($fst:ident, $snd:ident, $body:expr, $p:expr) => { + { let ($fst, $snd) = $p; $body } + } +} + +fn __mk_pair<A: Copy, B: Copy>(a: A, b: B) -> __pair<A, B> { (a, b) } + +fn hint_app<TArg, TRet>(f: &dyn Fn(TArg) -> TRet) -> &dyn Fn(TArg) -> TRet { + f +} + +#[derive(Debug, Clone)] +pub enum Coq_Init_Datatypes_list<'a, A> { + nil(PhantomData<&'a A>), + cons(PhantomData<&'a A>, A, &'a Coq_Init_Datatypes_list<'a, A>) +} + +type CertiCoq_Benchmarks_lib_Binom_key<'a> = u64; + +#[derive(Debug, Clone)] +pub enum CertiCoq_Benchmarks_lib_Binom_tree<'a> { + Node(PhantomData<&'a ()>, CertiCoq_Benchmarks_lib_Binom_key<'a>, &'a CertiCoq_Benchmarks_lib_Binom_tree<'a>, &'a CertiCoq_Benchmarks_lib_Binom_tree<'a>), + Leaf(PhantomData<&'a ()>) +} + +type CertiCoq_Benchmarks_lib_Binom_priqueue<'a> = &'a Coq_Init_Datatypes_list<'a, &'a CertiCoq_Benchmarks_lib_Binom_tree<'a>>; + +struct Program { +} + +impl<'a> Program { +fn new() -> Self { + Program { + } +} + +fn alloc<T>(&'a self, t: T) -> &'a T { + let _alloc = Box::new(t); + Box::leak(_alloc) +} + +fn closure<TArg, TRet>(&'a self, f: impl Fn(TArg) -> TRet + 'a) -> &'a dyn Fn(TArg) -> TRet { + let _alloc = Box::new(f); + Box::leak(_alloc) +} + +fn Coq_Init_Nat_leb(&'a self, n: u64, m: u64) -> bool { + __nat_elim!( + { + true + }, + n2, { + __nat_elim!( + { + false + }, + m2, { + self.Coq_Init_Nat_leb( + n2, + m2) + }, + m) + }, + n) +} +fn Coq_Init_Nat_leb__curried(&'a self) -> &'a dyn Fn(u64) -> &'a dyn Fn(u64) -> bool { + self.closure(move |n| { + self.closure(move |m| { + self.Coq_Init_Nat_leb( + n, + m) + }) + }) +} + +fn Coq_Init_Nat_ltb(&'a self, n: u64, m: u64) -> bool { + self.Coq_Init_Nat_leb( + __nat_succ( + n), + m) +} +fn Coq_Init_Nat_ltb__curried(&'a self) -> &'a dyn Fn(u64) -> &'a dyn Fn(u64) -> bool { + self.closure(move |n| { + self.closure(move |m| { + self.Coq_Init_Nat_ltb( + n, + m) + }) + }) +} + +fn CertiCoq_Benchmarks_lib_Binom_smash(&'a self, t: &'a CertiCoq_Benchmarks_lib_Binom_tree<'a>, u: &'a CertiCoq_Benchmarks_lib_Binom_tree<'a>) -> &'a CertiCoq_Benchmarks_lib_Binom_tree<'a> { + match t { + &CertiCoq_Benchmarks_lib_Binom_tree::Node(_, x, t1, t0) => { + match t0 { + &CertiCoq_Benchmarks_lib_Binom_tree::Node(_, k, t2, t3) => { + self.alloc( + CertiCoq_Benchmarks_lib_Binom_tree::Leaf( + PhantomData)) + }, + &CertiCoq_Benchmarks_lib_Binom_tree::Leaf(_) => { + match u { + &CertiCoq_Benchmarks_lib_Binom_tree::Node(_, y, u1, t2) => { + match t2 { + &CertiCoq_Benchmarks_lib_Binom_tree::Node(_, k, t3, t4) => { + self.alloc( + CertiCoq_Benchmarks_lib_Binom_tree::Leaf( + PhantomData)) + }, + &CertiCoq_Benchmarks_lib_Binom_tree::Leaf(_) => { + match self.Coq_Init_Nat_ltb( + y, + x) { + true => { + self.alloc( + CertiCoq_Benchmarks_lib_Binom_tree::Node( + PhantomData, + x, + self.alloc( + CertiCoq_Benchmarks_lib_Binom_tree::Node( + PhantomData, + y, + u1, + t1)), + self.alloc( + CertiCoq_Benchmarks_lib_Binom_tree::Leaf( + PhantomData)))) + }, + false => { + self.alloc( + CertiCoq_Benchmarks_lib_Binom_tree::Node( + PhantomData, + y, + self.alloc( + CertiCoq_Benchmarks_lib_Binom_tree::Node( + PhantomData, + x, + t1, + u1)), + self.alloc( + CertiCoq_Benchmarks_lib_Binom_tree::Leaf( + PhantomData)))) + }, + } + }, + } + }, + &CertiCoq_Benchmarks_lib_Binom_tree::Leaf(_) => { + self.alloc( + CertiCoq_Benchmarks_lib_Binom_tree::Leaf( + PhantomData)) + }, + } + }, + } + }, + &CertiCoq_Benchmarks_lib_Binom_tree::Leaf(_) => { + self.alloc( + CertiCoq_Benchmarks_lib_Binom_tree::Leaf( + PhantomData)) + }, + } +} +fn CertiCoq_Benchmarks_lib_Binom_smash__curried(&'a self) -> &'a dyn Fn(&'a CertiCoq_Benchmarks_lib_Binom_tree<'a>) -> &'a dyn Fn(&'a CertiCoq_Benchmarks_lib_Binom_tree<'a>) -> &'a CertiCoq_Benchmarks_lib_Binom_tree<'a> { + self.closure(move |t| { + self.closure(move |u| { + self.CertiCoq_Benchmarks_lib_Binom_smash( + t, + u) + }) + }) +} + +fn CertiCoq_Benchmarks_lib_Binom_carry(&'a self, q: &'a Coq_Init_Datatypes_list<'a, &'a CertiCoq_Benchmarks_lib_Binom_tree<'a>>, t: &'a CertiCoq_Benchmarks_lib_Binom_tree<'a>) -> &'a Coq_Init_Datatypes_list<'a, &'a CertiCoq_Benchmarks_lib_Binom_tree<'a>> { + match q { + &Coq_Init_Datatypes_list::nil(_) => { + match t { + &CertiCoq_Benchmarks_lib_Binom_tree::Node(_, k, t0, t1) => { + self.alloc( + Coq_Init_Datatypes_list::cons( + PhantomData, + t, + self.alloc( + Coq_Init_Datatypes_list::nil( + PhantomData)))) + }, + &CertiCoq_Benchmarks_lib_Binom_tree::Leaf(_) => { + self.alloc( + Coq_Init_Datatypes_list::nil( + PhantomData)) + }, + } + }, + &Coq_Init_Datatypes_list::cons(_, u, q2) => { + match u { + &CertiCoq_Benchmarks_lib_Binom_tree::Node(_, k, t0, t1) => { + match t { + &CertiCoq_Benchmarks_lib_Binom_tree::Node(_, k0, t2, t3) => { + self.alloc( + Coq_Init_Datatypes_list::cons( + PhantomData, + self.alloc( + CertiCoq_Benchmarks_lib_Binom_tree::Leaf( + PhantomData)), + self.CertiCoq_Benchmarks_lib_Binom_carry( + q2, + self.CertiCoq_Benchmarks_lib_Binom_smash( + t, + u)))) + }, + &CertiCoq_Benchmarks_lib_Binom_tree::Leaf(_) => { + self.alloc( + Coq_Init_Datatypes_list::cons( + PhantomData, + u, + q2)) + }, + } + }, + &CertiCoq_Benchmarks_lib_Binom_tree::Leaf(_) => { + self.alloc( + Coq_Init_Datatypes_list::cons( + PhantomData, + t, + q2)) + }, + } + }, + } +} +fn CertiCoq_Benchmarks_lib_Binom_carry__curried(&'a self) -> &'a dyn Fn(&'a Coq_Init_Datatypes_list<'a, &'a CertiCoq_Benchmarks_lib_Binom_tree<'a>>) -> &'a dyn Fn(&'a CertiCoq_Benchmarks_lib_Binom_tree<'a>) -> &'a Coq_Init_Datatypes_list<'a, &'a CertiCoq_Benchmarks_lib_Binom_tree<'a>> { + self.closure(move |q| { + self.closure(move |t| { + self.CertiCoq_Benchmarks_lib_Binom_carry( + q, + t) + }) + }) +} + +fn CertiCoq_Benchmarks_lib_Binom_insert(&'a self, x: CertiCoq_Benchmarks_lib_Binom_key<'a>, q: CertiCoq_Benchmarks_lib_Binom_priqueue<'a>) -> CertiCoq_Benchmarks_lib_Binom_priqueue<'a> { + self.CertiCoq_Benchmarks_lib_Binom_carry( + q, + self.alloc( + CertiCoq_Benchmarks_lib_Binom_tree::Node( + PhantomData, + x, + self.alloc( + CertiCoq_Benchmarks_lib_Binom_tree::Leaf( + PhantomData)), + self.alloc( + CertiCoq_Benchmarks_lib_Binom_tree::Leaf( + PhantomData))))) +} +fn CertiCoq_Benchmarks_lib_Binom_insert__curried(&'a self) -> &'a dyn Fn(CertiCoq_Benchmarks_lib_Binom_key<'a>) -> &'a dyn Fn(CertiCoq_Benchmarks_lib_Binom_priqueue<'a>) -> CertiCoq_Benchmarks_lib_Binom_priqueue<'a> { + self.closure(move |x| { + self.closure(move |q| { + self.CertiCoq_Benchmarks_lib_Binom_insert( + x, + q) + }) + }) +} + +fn CertiCoq_Benchmarks_lib_Binom_insert_list(&'a self, l: &'a Coq_Init_Datatypes_list<'a, u64>, q: CertiCoq_Benchmarks_lib_Binom_priqueue<'a>) -> CertiCoq_Benchmarks_lib_Binom_priqueue<'a> { + match l { + &Coq_Init_Datatypes_list::nil(_) => { + q + }, + &Coq_Init_Datatypes_list::cons(_, x, l2) => { + self.CertiCoq_Benchmarks_lib_Binom_insert_list( + l2, + self.CertiCoq_Benchmarks_lib_Binom_insert( + x, + q)) + }, + } +} +fn CertiCoq_Benchmarks_lib_Binom_insert_list__curried(&'a self) -> &'a dyn Fn(&'a Coq_Init_Datatypes_list<'a, u64>) -> &'a dyn Fn(CertiCoq_Benchmarks_lib_Binom_priqueue<'a>) -> CertiCoq_Benchmarks_lib_Binom_priqueue<'a> { + self.closure(move |l| { + self.closure(move |q| { + self.CertiCoq_Benchmarks_lib_Binom_insert_list( + l, + q) + }) + }) +} + +fn CertiCoq_Benchmarks_lib_Binom_make_list(&'a self, n: u64, l: &'a Coq_Init_Datatypes_list<'a, u64>) -> &'a Coq_Init_Datatypes_list<'a, u64> { + __nat_elim!( + { + self.alloc( + Coq_Init_Datatypes_list::cons( + PhantomData, + 0, + l)) + }, + n0, { + __nat_elim!( + { + self.alloc( + Coq_Init_Datatypes_list::cons( + PhantomData, + __nat_succ( + 0), + l)) + }, + n2, { + self.CertiCoq_Benchmarks_lib_Binom_make_list( + n2, + self.alloc( + Coq_Init_Datatypes_list::cons( + PhantomData, + __nat_succ( + __nat_succ( + n2)), + l))) + }, + n0) + }, + n) +} +fn CertiCoq_Benchmarks_lib_Binom_make_list__curried(&'a self) -> &'a dyn Fn(u64) -> &'a dyn Fn(&'a Coq_Init_Datatypes_list<'a, u64>) -> &'a Coq_Init_Datatypes_list<'a, u64> { + self.closure(move |n| { + self.closure(move |l| { + self.CertiCoq_Benchmarks_lib_Binom_make_list( + n, + l) + }) + }) +} + +fn CertiCoq_Benchmarks_lib_Binom_empty(&'a self) -> CertiCoq_Benchmarks_lib_Binom_priqueue<'a> { + self.alloc( + Coq_Init_Datatypes_list::nil( + PhantomData)) +} + +fn CertiCoq_Benchmarks_lib_Binom_join(&'a self, p: CertiCoq_Benchmarks_lib_Binom_priqueue<'a>, q: CertiCoq_Benchmarks_lib_Binom_priqueue<'a>, c: &'a CertiCoq_Benchmarks_lib_Binom_tree<'a>) -> CertiCoq_Benchmarks_lib_Binom_priqueue<'a> { + match p { + &Coq_Init_Datatypes_list::nil(_) => { + self.CertiCoq_Benchmarks_lib_Binom_carry( + q, + c) + }, + &Coq_Init_Datatypes_list::cons(_, p1, p2) => { + match p1 { + &CertiCoq_Benchmarks_lib_Binom_tree::Node(_, k, t, t0) => { + match q { + &Coq_Init_Datatypes_list::nil(_) => { + self.CertiCoq_Benchmarks_lib_Binom_carry( + p, + c) + }, + &Coq_Init_Datatypes_list::cons(_, q1, q2) => { + match q1 { + &CertiCoq_Benchmarks_lib_Binom_tree::Node(_, k0, t1, t2) => { + self.alloc( + Coq_Init_Datatypes_list::cons( + PhantomData, + c, + self.CertiCoq_Benchmarks_lib_Binom_join( + p2, + q2, + self.CertiCoq_Benchmarks_lib_Binom_smash( + p1, + q1)))) + }, + &CertiCoq_Benchmarks_lib_Binom_tree::Leaf(_) => { + match c { + &CertiCoq_Benchmarks_lib_Binom_tree::Node(_, k0, t1, t2) => { + self.alloc( + Coq_Init_Datatypes_list::cons( + PhantomData, + self.alloc( + CertiCoq_Benchmarks_lib_Binom_tree::Leaf( + PhantomData)), + self.CertiCoq_Benchmarks_lib_Binom_join( + p2, + q2, + self.CertiCoq_Benchmarks_lib_Binom_smash( + c, + p1)))) + }, + &CertiCoq_Benchmarks_lib_Binom_tree::Leaf(_) => { + self.alloc( + Coq_Init_Datatypes_list::cons( + PhantomData, + p1, + self.CertiCoq_Benchmarks_lib_Binom_join( + p2, + q2, + self.alloc( + CertiCoq_Benchmarks_lib_Binom_tree::Leaf( + PhantomData))))) + }, + } + }, + } + }, + } + }, + &CertiCoq_Benchmarks_lib_Binom_tree::Leaf(_) => { + match q { + &Coq_Init_Datatypes_list::nil(_) => { + self.CertiCoq_Benchmarks_lib_Binom_carry( + p, + c) + }, + &Coq_Init_Datatypes_list::cons(_, q1, q2) => { + match q1 { + &CertiCoq_Benchmarks_lib_Binom_tree::Node(_, k, t, t0) => { + match c { + &CertiCoq_Benchmarks_lib_Binom_tree::Node(_, k0, t1, t2) => { + self.alloc( + Coq_Init_Datatypes_list::cons( + PhantomData, + self.alloc( + CertiCoq_Benchmarks_lib_Binom_tree::Leaf( + PhantomData)), + self.CertiCoq_Benchmarks_lib_Binom_join( + p2, + q2, + self.CertiCoq_Benchmarks_lib_Binom_smash( + c, + q1)))) + }, + &CertiCoq_Benchmarks_lib_Binom_tree::Leaf(_) => { + self.alloc( + Coq_Init_Datatypes_list::cons( + PhantomData, + q1, + self.CertiCoq_Benchmarks_lib_Binom_join( + p2, + q2, + self.alloc( + CertiCoq_Benchmarks_lib_Binom_tree::Leaf( + PhantomData))))) + }, + } + }, + &CertiCoq_Benchmarks_lib_Binom_tree::Leaf(_) => { + self.alloc( + Coq_Init_Datatypes_list::cons( + PhantomData, + c, + self.CertiCoq_Benchmarks_lib_Binom_join( + p2, + q2, + self.alloc( + CertiCoq_Benchmarks_lib_Binom_tree::Leaf( + PhantomData))))) + }, + } + }, + } + }, + } + }, + } +} +fn CertiCoq_Benchmarks_lib_Binom_join__curried(&'a self) -> &'a dyn Fn(CertiCoq_Benchmarks_lib_Binom_priqueue<'a>) -> &'a dyn Fn(CertiCoq_Benchmarks_lib_Binom_priqueue<'a>) -> &'a dyn Fn(&'a CertiCoq_Benchmarks_lib_Binom_tree<'a>) -> CertiCoq_Benchmarks_lib_Binom_priqueue<'a> { + self.closure(move |p| { + self.closure(move |q| { + self.closure(move |c| { + self.CertiCoq_Benchmarks_lib_Binom_join( + p, + q, + c) + }) + }) + }) +} + +fn CertiCoq_Benchmarks_lib_Binom_merge(&'a self, p: CertiCoq_Benchmarks_lib_Binom_priqueue<'a>, q: CertiCoq_Benchmarks_lib_Binom_priqueue<'a>) -> CertiCoq_Benchmarks_lib_Binom_priqueue<'a> { + self.CertiCoq_Benchmarks_lib_Binom_join( + p, + q, + self.alloc( + CertiCoq_Benchmarks_lib_Binom_tree::Leaf( + PhantomData))) +} +fn CertiCoq_Benchmarks_lib_Binom_merge__curried(&'a self) -> &'a dyn Fn(CertiCoq_Benchmarks_lib_Binom_priqueue<'a>) -> &'a dyn Fn(CertiCoq_Benchmarks_lib_Binom_priqueue<'a>) -> CertiCoq_Benchmarks_lib_Binom_priqueue<'a> { + self.closure(move |p| { + self.closure(move |q| { + self.CertiCoq_Benchmarks_lib_Binom_merge( + p, + q) + }) + }) +} + +fn CertiCoq_Benchmarks_lib_Binom_find_max_(&'a self, current: CertiCoq_Benchmarks_lib_Binom_key<'a>, q: CertiCoq_Benchmarks_lib_Binom_priqueue<'a>) -> CertiCoq_Benchmarks_lib_Binom_key<'a> { + match q { + &Coq_Init_Datatypes_list::nil(_) => { + current + }, + &Coq_Init_Datatypes_list::cons(_, t, q2) => { + match t { + &CertiCoq_Benchmarks_lib_Binom_tree::Node(_, x, t0, t1) => { + self.CertiCoq_Benchmarks_lib_Binom_find_max_( + match self.Coq_Init_Nat_ltb( + current, + x) { + true => { + x + }, + false => { + current + }, + }, + q2) + }, + &CertiCoq_Benchmarks_lib_Binom_tree::Leaf(_) => { + self.CertiCoq_Benchmarks_lib_Binom_find_max_( + current, + q2) + }, + } + }, + } +} +fn CertiCoq_Benchmarks_lib_Binom_find_max___curried(&'a self) -> &'a dyn Fn(CertiCoq_Benchmarks_lib_Binom_key<'a>) -> &'a dyn Fn(CertiCoq_Benchmarks_lib_Binom_priqueue<'a>) -> CertiCoq_Benchmarks_lib_Binom_key<'a> { + self.closure(move |current| { + self.closure(move |q| { + self.CertiCoq_Benchmarks_lib_Binom_find_max_( + current, + q) + }) + }) +} + +fn CertiCoq_Benchmarks_lib_Binom_find_max(&'a self, q: CertiCoq_Benchmarks_lib_Binom_priqueue<'a>) -> Option<CertiCoq_Benchmarks_lib_Binom_key<'a>> { + match q { + &Coq_Init_Datatypes_list::nil(_) => { + None + }, + &Coq_Init_Datatypes_list::cons(_, t, q2) => { + match t { + &CertiCoq_Benchmarks_lib_Binom_tree::Node(_, x, t0, t1) => { + Some( + self.CertiCoq_Benchmarks_lib_Binom_find_max_( + x, + q2)) + }, + &CertiCoq_Benchmarks_lib_Binom_tree::Leaf(_) => { + self.CertiCoq_Benchmarks_lib_Binom_find_max( + q2) + }, + } + }, + } +} +fn CertiCoq_Benchmarks_lib_Binom_find_max__curried(&'a self) -> &'a dyn Fn(CertiCoq_Benchmarks_lib_Binom_priqueue<'a>) -> Option<CertiCoq_Benchmarks_lib_Binom_key<'a>> { + self.closure(move |q| { + self.CertiCoq_Benchmarks_lib_Binom_find_max( + q) + }) +} + +fn CertiCoq_Benchmarks_lib_Binom_unzip(&'a self, t: &'a CertiCoq_Benchmarks_lib_Binom_tree<'a>, cont: &'a dyn Fn(CertiCoq_Benchmarks_lib_Binom_priqueue<'a>) -> CertiCoq_Benchmarks_lib_Binom_priqueue<'a>) -> CertiCoq_Benchmarks_lib_Binom_priqueue<'a> { + match t { + &CertiCoq_Benchmarks_lib_Binom_tree::Node(_, x, t1, t2) => { + self.CertiCoq_Benchmarks_lib_Binom_unzip( + t2, + self.closure(move |q| { + self.alloc( + Coq_Init_Datatypes_list::cons( + PhantomData, + self.alloc( + CertiCoq_Benchmarks_lib_Binom_tree::Node( + PhantomData, + x, + t1, + self.alloc( + CertiCoq_Benchmarks_lib_Binom_tree::Leaf( + PhantomData)))), + hint_app(cont)(q))) + })) + }, + &CertiCoq_Benchmarks_lib_Binom_tree::Leaf(_) => { + hint_app(cont)(self.alloc( + Coq_Init_Datatypes_list::nil( + PhantomData))) + }, + } +} +fn CertiCoq_Benchmarks_lib_Binom_unzip__curried(&'a self) -> &'a dyn Fn(&'a CertiCoq_Benchmarks_lib_Binom_tree<'a>) -> &'a dyn Fn(&'a dyn Fn(CertiCoq_Benchmarks_lib_Binom_priqueue<'a>) -> CertiCoq_Benchmarks_lib_Binom_priqueue<'a>) -> CertiCoq_Benchmarks_lib_Binom_priqueue<'a> { + self.closure(move |t| { + self.closure(move |cont| { + self.CertiCoq_Benchmarks_lib_Binom_unzip( + t, + cont) + }) + }) +} + +fn CertiCoq_Benchmarks_lib_Binom_heap_delete_max(&'a self, t: &'a CertiCoq_Benchmarks_lib_Binom_tree<'a>) -> CertiCoq_Benchmarks_lib_Binom_priqueue<'a> { + match t { + &CertiCoq_Benchmarks_lib_Binom_tree::Node(_, x, t1, t0) => { + match t0 { + &CertiCoq_Benchmarks_lib_Binom_tree::Node(_, k, t2, t3) => { + self.alloc( + Coq_Init_Datatypes_list::nil( + PhantomData)) + }, + &CertiCoq_Benchmarks_lib_Binom_tree::Leaf(_) => { + self.CertiCoq_Benchmarks_lib_Binom_unzip( + t1, + self.closure(move |u| { + u + })) + }, + } + }, + &CertiCoq_Benchmarks_lib_Binom_tree::Leaf(_) => { + self.alloc( + Coq_Init_Datatypes_list::nil( + PhantomData)) + }, + } +} +fn CertiCoq_Benchmarks_lib_Binom_heap_delete_max__curried(&'a self) -> &'a dyn Fn(&'a CertiCoq_Benchmarks_lib_Binom_tree<'a>) -> CertiCoq_Benchmarks_lib_Binom_priqueue<'a> { + self.closure(move |t| { + self.CertiCoq_Benchmarks_lib_Binom_heap_delete_max( + t) + }) +} + +fn CertiCoq_Benchmarks_lib_Binom_delete_max_aux(&'a self, m: CertiCoq_Benchmarks_lib_Binom_key<'a>, p: CertiCoq_Benchmarks_lib_Binom_priqueue<'a>) -> __pair<CertiCoq_Benchmarks_lib_Binom_priqueue<'a>, CertiCoq_Benchmarks_lib_Binom_priqueue<'a>> { + match p { + &Coq_Init_Datatypes_list::nil(_) => { + __mk_pair( + self.alloc( + Coq_Init_Datatypes_list::nil( + PhantomData)), + self.alloc( + Coq_Init_Datatypes_list::nil( + PhantomData))) + }, + &Coq_Init_Datatypes_list::cons(_, t, p2) => { + match t { + &CertiCoq_Benchmarks_lib_Binom_tree::Node(_, x, t1, t0) => { + match t0 { + &CertiCoq_Benchmarks_lib_Binom_tree::Node(_, k, t2, t3) => { + __mk_pair( + self.alloc( + Coq_Init_Datatypes_list::nil( + PhantomData)), + self.alloc( + Coq_Init_Datatypes_list::nil( + PhantomData))) + }, + &CertiCoq_Benchmarks_lib_Binom_tree::Leaf(_) => { + match self.Coq_Init_Nat_ltb( + x, + m) { + true => { + __pair_elim!( + k, j, { + __mk_pair( + self.alloc( + Coq_Init_Datatypes_list::cons( + PhantomData, + self.alloc( + CertiCoq_Benchmarks_lib_Binom_tree::Node( + PhantomData, + x, + t1, + self.alloc( + CertiCoq_Benchmarks_lib_Binom_tree::Leaf( + PhantomData)))), + k)), + j) + }, + self.CertiCoq_Benchmarks_lib_Binom_delete_max_aux( + m, + p2)) + }, + false => { + __mk_pair( + self.alloc( + Coq_Init_Datatypes_list::cons( + PhantomData, + self.alloc( + CertiCoq_Benchmarks_lib_Binom_tree::Leaf( + PhantomData)), + p2)), + self.CertiCoq_Benchmarks_lib_Binom_heap_delete_max( + self.alloc( + CertiCoq_Benchmarks_lib_Binom_tree::Node( + PhantomData, + x, + t1, + self.alloc( + CertiCoq_Benchmarks_lib_Binom_tree::Leaf( + PhantomData)))))) + }, + } + }, + } + }, + &CertiCoq_Benchmarks_lib_Binom_tree::Leaf(_) => { + __pair_elim!( + k, j, { + __mk_pair( + self.alloc( + Coq_Init_Datatypes_list::cons( + PhantomData, + self.alloc( + CertiCoq_Benchmarks_lib_Binom_tree::Leaf( + PhantomData)), + k)), + j) + }, + self.CertiCoq_Benchmarks_lib_Binom_delete_max_aux( + m, + p2)) + }, + } + }, + } +} +fn CertiCoq_Benchmarks_lib_Binom_delete_max_aux__curried(&'a self) -> &'a dyn Fn(CertiCoq_Benchmarks_lib_Binom_key<'a>) -> &'a dyn Fn(CertiCoq_Benchmarks_lib_Binom_priqueue<'a>) -> __pair<CertiCoq_Benchmarks_lib_Binom_priqueue<'a>, CertiCoq_Benchmarks_lib_Binom_priqueue<'a>> { + self.closure(move |m| { + self.closure(move |p| { + self.CertiCoq_Benchmarks_lib_Binom_delete_max_aux( + m, + p) + }) + }) +} + +fn CertiCoq_Benchmarks_lib_Binom_delete_max(&'a self, q: CertiCoq_Benchmarks_lib_Binom_priqueue<'a>) -> Option<__pair<CertiCoq_Benchmarks_lib_Binom_key<'a>, CertiCoq_Benchmarks_lib_Binom_priqueue<'a>>> { + match self.CertiCoq_Benchmarks_lib_Binom_find_max( + q) { + Some(m) => { + __pair_elim!( + q2, p, { + Some( + __mk_pair( + m, + self.CertiCoq_Benchmarks_lib_Binom_join( + q2, + p, + self.alloc( + CertiCoq_Benchmarks_lib_Binom_tree::Leaf( + PhantomData))))) + }, + self.CertiCoq_Benchmarks_lib_Binom_delete_max_aux( + m, + q)) + }, + None => { + None + }, + } +} +fn CertiCoq_Benchmarks_lib_Binom_delete_max__curried(&'a self) -> &'a dyn Fn(CertiCoq_Benchmarks_lib_Binom_priqueue<'a>) -> Option<__pair<CertiCoq_Benchmarks_lib_Binom_key<'a>, CertiCoq_Benchmarks_lib_Binom_priqueue<'a>>> { + self.closure(move |q| { + self.CertiCoq_Benchmarks_lib_Binom_delete_max( + q) + }) +} + +fn CertiCoq_Benchmarks_lib_Binom_main(&'a self) -> CertiCoq_Benchmarks_lib_Binom_key<'a> { + let a = + self.CertiCoq_Benchmarks_lib_Binom_insert_list( + self.CertiCoq_Benchmarks_lib_Binom_make_list( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + 0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))), + self.alloc( + Coq_Init_Datatypes_list::nil( + PhantomData))), + self.CertiCoq_Benchmarks_lib_Binom_empty()); + let b = + self.CertiCoq_Benchmarks_lib_Binom_insert_list( + self.CertiCoq_Benchmarks_lib_Binom_make_list( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + __nat_succ( + 0))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))), + self.alloc( + Coq_Init_Datatypes_list::nil( + PhantomData))), + self.CertiCoq_Benchmarks_lib_Binom_empty()); + let c = + self.CertiCoq_Benchmarks_lib_Binom_merge( + a, + b); + match self.CertiCoq_Benchmarks_lib_Binom_delete_max( + c) { + Some(p) => { + __pair_elim!( + p0, k, { + p0 + }, + p) + }, + None => { + 0 + }, + } +} + +fn CertiCoq_Benchmarks_tests_binom(&'a self) -> CertiCoq_Benchmarks_lib_Binom_key<'a> { + self.CertiCoq_Benchmarks_lib_Binom_main() +} +} +fn main() { + println!("{:?}", Program::new().CertiCoq_Benchmarks_tests_binom()) +} diff --git a/tests/ui/pattern/patkind-ref-binding-issue-114896.fixed b/tests/ui/pattern/patkind-ref-binding-issue-114896.fixed new file mode 100644 index 00000000000..086a119eb77 --- /dev/null +++ b/tests/ui/pattern/patkind-ref-binding-issue-114896.fixed @@ -0,0 +1,10 @@ +//@ run-rustfix +#![allow(dead_code)] + +fn main() { + fn x(a: &char) { + let &(mut b) = a; + b.make_ascii_uppercase(); +//~^ cannot borrow `b` as mutable, as it is not declared as mutable + } +} diff --git a/tests/ui/pattern/issue-114896.rs b/tests/ui/pattern/patkind-ref-binding-issue-114896.rs index cde37f658d6..b4d6b72c01f 100644 --- a/tests/ui/pattern/issue-114896.rs +++ b/tests/ui/pattern/patkind-ref-binding-issue-114896.rs @@ -1,3 +1,6 @@ +//@ run-rustfix +#![allow(dead_code)] + fn main() { fn x(a: &char) { let &b = a; diff --git a/tests/ui/pattern/issue-114896.stderr b/tests/ui/pattern/patkind-ref-binding-issue-114896.stderr index 285c9109e1b..68538255edd 100644 --- a/tests/ui/pattern/issue-114896.stderr +++ b/tests/ui/pattern/patkind-ref-binding-issue-114896.stderr @@ -1,5 +1,5 @@ error[E0596]: cannot borrow `b` as mutable, as it is not declared as mutable - --> $DIR/issue-114896.rs:4:9 + --> $DIR/patkind-ref-binding-issue-114896.rs:7:9 | LL | let &b = a; | -- help: consider changing this to be mutable: `&(mut b)` diff --git a/tests/ui/pattern/patkind-ref-binding-issue-122415.fixed b/tests/ui/pattern/patkind-ref-binding-issue-122415.fixed new file mode 100644 index 00000000000..6144f062169 --- /dev/null +++ b/tests/ui/pattern/patkind-ref-binding-issue-122415.fixed @@ -0,0 +1,11 @@ +//@ run-rustfix +#![allow(dead_code)] + +fn mutate(_y: &mut i32) {} + +fn foo(&(mut x): &i32) { + mutate(&mut x); + //~^ ERROR cannot borrow `x` as mutable +} + +fn main() {} diff --git a/tests/ui/pattern/patkind-ref-binding-issue-122415.rs b/tests/ui/pattern/patkind-ref-binding-issue-122415.rs new file mode 100644 index 00000000000..b9f6416027a --- /dev/null +++ b/tests/ui/pattern/patkind-ref-binding-issue-122415.rs @@ -0,0 +1,11 @@ +//@ run-rustfix +#![allow(dead_code)] + +fn mutate(_y: &mut i32) {} + +fn foo(&x: &i32) { + mutate(&mut x); + //~^ ERROR cannot borrow `x` as mutable +} + +fn main() {} diff --git a/tests/ui/pattern/patkind-ref-binding-issue-122415.stderr b/tests/ui/pattern/patkind-ref-binding-issue-122415.stderr new file mode 100644 index 00000000000..39283133ac7 --- /dev/null +++ b/tests/ui/pattern/patkind-ref-binding-issue-122415.stderr @@ -0,0 +1,11 @@ +error[E0596]: cannot borrow `x` as mutable, as it is not declared as mutable + --> $DIR/patkind-ref-binding-issue-122415.rs:7:12 + | +LL | fn foo(&x: &i32) { + | -- help: consider changing this to be mutable: `&(mut x)` +LL | mutate(&mut x); + | ^^^^^^ cannot borrow as mutable + +error: aborting due to 1 previous error + +For more information about this error, try `rustc --explain E0596`. |