diff --git a/lean-toolchain b/lean-toolchain index 18640c8b0..2694eb767 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.31.0 +leanprover/lean4:v4.32.0-rc1 diff --git a/makeTables.lean b/makeTables.lean index 4beb0a710..a04e40a2b 100644 --- a/makeTables.lean +++ b/makeTables.lean @@ -374,7 +374,7 @@ def mkNumericValue : IO <| Array (UInt32 × UInt32 × NumericType) := do for d in UnicodeData.data do match d.numeric with | some (.decimal 0) => - t := t.push (d.code, d.code + 9, .decimal 0) + t := t.push (d.code, d.code + 9, NumericType.decimal 0) | some (.digit v) => match t.back! with | (c₀, c₁, n@(NumericType.digit x)) =>