fact: Fixpoint compile_nat {var} (n : nat) : @expr var := match n with | O => NatO | S x => NatS (compile_nat x) end.
imports: Coq.quote.Quote Reify.ReifyCommon Coq.NArith.NArith PerformanceExperiments.Harness Reify.BenchmarkExtraUtil