fact: Fixpoint compile {var} (e : qexpr) : @expr var := match e with | qNatO => NatO | qNatS x => NatS (compile x) | qNatMul x y => NatMul (compile x) (compile y) | qConst k => compile_nat k end.
imports: Coq.quote.Quote Reify.ReifyCommon Coq.NArith.NArith PerformanceExperiments.Harness Reify.BenchmarkExtraUtil