diff --git a/src/Init/Data/Repr.lean b/src/Init/Data/Repr.lean index 83d775c3fa8f6..ddc72999bdf35 100644 --- a/src/Init/Data/Repr.lean +++ b/src/Init/Data/Repr.lean @@ -121,7 +121,17 @@ def toDigits (base : Nat) (n : Nat) : List Char := toDigitsCore base (n+1) n [] @[extern "lean_string_of_nat"] -protected def repr (n : @& Nat) : String := +private opaque reprFastAux (n : @& Nat) : String + +private def reprArray : Array String := Id.run do + List.range 128 |>.map Nat.reprFastAux |> Array.mk + +private def reprFast (n : Nat) : String := + if h : n < 128 then Nat.reprArray.get ⟨n, h⟩ else + Nat.reprFastAux n + +@[implemented_by reprFast] +protected def repr (n : Nat) : String := (toDigits 10 n).asString def superDigitChar (n : Nat) : Char := diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h index 0699845ba4526..cb8a954a4d164 100644 --- a/stage0/src/stdlib_flags.h +++ b/stage0/src/stdlib_flags.h @@ -6,7 +6,7 @@ options get_default_options() { // see https://lean-lang.org/lean4/doc/dev/bootstrap.html#further-bootstrapping-complications #if LEAN_IS_STAGE0 == 1 // switch to `true` for ABI-breaking changes affecting meta code - opts = opts.update({"interpreter", "prefer_native"}, false); + opts = opts.update({"interpreter", "prefer_native"}, true); // switch to `true` for changing built-in parsers used in quotations opts = opts.update({"internal", "parseQuotWithCurrentStage"}, false); // toggling `parseQuotWithCurrentStage` may also require toggling the following option if macros/syntax