.

This PR adjusts the way the pretty printer unresolves names. It used to
make use of all `export`s when pretty printing, but now it only uses
`export`s that put names into parent namespaces (heuristic: these are
"API exports" that are intended by the library author), rather than
"horizontal exports" that put the names into an unrelated namespace,
which the dot notation feature in #6189 now incentivizes.

Closes the already closed #2524

CODEOWNERS

@@ -4,7 +4,7 @@
 # Listed persons will automatically be asked by GitHub to review a PR touching these paths.
 # If multiple names are listed, a review by any of them is considered sufficient by default.
 
-/.github/ @Kha @kim-em
+/.github/ @kim-em
 /RELEASES.md @kim-em
 /src/kernel/ @leodemoura
 /src/lake/ @tydeu
@@ -14,9 +14,7 @@
 /src/Lean/Elab/Tactic/ @kim-em
 /src/Lean/Language/ @Kha
 /src/Lean/Meta/Tactic/ @leodemoura
-/src/Lean/Parser/ @Kha
-/src/Lean/PrettyPrinter/ @Kha
-/src/Lean/PrettyPrinter/Delaborator/ @kmill
+/src/Lean/PrettyPrinter/ @kmill
 /src/Lean/Server/ @mhuisi
 /src/Lean/Widget/ @Vtec234
 /src/Init/Data/ @kim-em

RELEASES.md

@@ -21,7 +21,286 @@ Release candidate, release notes will be copied from the branch `releases/v4.15.
 v4.14.0
 ----------
 
-Release candidate, release notes will be copied from the branch `releases/v4.14.0` once completed.
+**Full Changelog**: https://github.com/leanprover/lean4/compare/v4.13.0...v4.14.0
+
+### Language features, tactics, and metaprograms
+
+* `structure` and `inductive` commands
+  * [#5517](https://github.com/leanprover/lean4/pull/5517) improves universe level inference for the resulting type of an `inductive` or `structure.` Recall that a `Prop`-valued inductive type is a syntactic subsingleton if it has at most one constructor and all the arguments to the constructor are in `Prop`. Such types have large elimination, so they could be defined in `Type` or `Prop` without any trouble. The way inference has changed is that if a type is a syntactic subsingleton with exactly one constructor, and the constructor has at least one parameter/field, then the `inductive`/`structure` command will prefer creating a `Prop` instead of a `Type`. The upshot is that the `: Prop` in `structure S : Prop` is often no longer needed. (With @arthur-adjedj).
+  * [#5842](https://github.com/leanprover/lean4/pull/5842) and [#5783](https://github.com/leanprover/lean4/pull/5783) implement a feature where the `structure` command can now define recursive inductive types:
+    ```lean
+    structure Tree where
+      n : Nat
+      children : Fin n → Tree
+
+    def Tree.size : Tree → Nat
+      | {n, children} => Id.run do
+        let mut s := 0
+        for h : i in [0 : n] do
+          s := s + (children ⟨i, h.2⟩).size
+        pure s
+    ```
+  * [#5814](https://github.com/leanprover/lean4/pull/5814) fixes a bug where Mathlib's `Type*` elaborator could lead to incorrect universe parameters with the `inductive` command.
+  * [#3152](https://github.com/leanprover/lean4/pull/3152) and [#5844](https://github.com/leanprover/lean4/pull/5844) fix bugs in default value processing for structure instance notation (with @arthur-adjedj).
+  * [#5399](https://github.com/leanprover/lean4/pull/5399) promotes instance synthesis order calculation failure from a soft error to a hard error.
+  * [#5542](https://github.com/leanprover/lean4/pull/5542) deprecates `:=` variants of `inductive` and `structure` (see breaking changes).
+
+* **Application elaboration improvements**
+  * [#5671](https://github.com/leanprover/lean4/pull/5671) makes `@[elab_as_elim]` require at least one discriminant, since otherwise there is no advantage to this alternative elaborator.
+  * [#5528](https://github.com/leanprover/lean4/pull/5528) enables field notation in explicit mode. The syntax `@x.f` elaborates as `@S.f` with `x` supplied to the appropriate parameter.
+  * [#5692](https://github.com/leanprover/lean4/pull/5692) modifies the dot notation resolution algorithm so that it can apply `CoeFun` instances. For example, Mathlib has `Multiset.card : Multiset α →+ Nat`, and now with `m : Multiset α`, the notation `m.card` resolves to `⇑Multiset.card m`.
+  * [#5658](https://github.com/leanprover/lean4/pull/5658) fixes a bug where 'don't know how to synthesize implicit argument' errors might have the incorrect local context when the eta arguments feature is activated.
+  * [#5933](https://github.com/leanprover/lean4/pull/5933) fixes a bug where `..` ellipses in patterns made use of optparams and autoparams.
+  * [#5770](https://github.com/leanprover/lean4/pull/5770) makes dot notation for structures resolve using *all* ancestors. Adds a *resolution order* for generalized field notation. This is the order of namespaces visited during resolution when trying to resolve names. The algorithm to compute a resolution order is the commonly used C3 linearization (used for example by Python), which when successful ensures that immediate parents' namespaces are considered before more distant ancestors' namespaces. By default we use a relaxed version of the algorithm that tolerates inconsistencies, but using `set_option structure.strictResolutionOrder true` makes inconsistent parent orderings into warnings.
+
+* **Recursion and induction principles**
+  * [#5619](https://github.com/leanprover/lean4/pull/5619) fixes functional induction principle generation to avoid over-eta-expanding in the preprocessing step.
+  * [#5766](https://github.com/leanprover/lean4/pull/5766) fixes structural nested recursion so that it is not confused when a nested type appears first.
+  * [#5803](https://github.com/leanprover/lean4/pull/5803) fixes a bug in functional induction principle generation when there are `let` bindings.
+  * [#5904](https://github.com/leanprover/lean4/pull/5904) improves functional induction principle generation to unfold aux definitions more carefully.
+  * [#5850](https://github.com/leanprover/lean4/pull/5850) refactors code for `Predefinition.Structural`.
+
+* **Error messages**
+  * [#5276](https://github.com/leanprover/lean4/pull/5276) fixes a bug in "type mismatch" errors that would structurally assign metavariables during the algorithm to expose differences.
+  * [#5919](https://github.com/leanprover/lean4/pull/5919) makes "type mismatch" errors add type ascriptions to expose differences for numeric literals.
+  * [#5922](https://github.com/leanprover/lean4/pull/5922) makes "type mismatch" errors expose differences in the bodies of functions and pi types.
+  * [#5888](https://github.com/leanprover/lean4/pull/5888) improves the error message for invalid induction alternative names in `match` expressions (@josojo).
+  * [#5719](https://github.com/leanprover/lean4/pull/5719) improves `calc` error messages.
+
+* [#5627](https://github.com/leanprover/lean4/pull/5627) and [#5663](https://github.com/leanprover/lean4/pull/5663) improve the **`#eval` command** and introduce some new features.
+  * Now results can be pretty printed if there is a `ToExpr` instance, which means **hoverable output**. If `ToExpr` fails, it then tries looking for a `Repr` or `ToString` instance like before. Setting `set_option eval.pp false` disables making use of `ToExpr` instances.
+  * There is now **auto-derivation** of `Repr` instances, enabled with the `pp.derive.repr` option (default to **true**). For example:
+    ```lean
+    inductive Baz
+    | a | b
+
+    #eval Baz.a
+    -- Baz.a
+    ```
+    It simply does `deriving instance Repr for Baz` when there's no way to represent `Baz`.
+  * The option `eval.type` controls whether or not to include the type in the output. For now the default is false.
+  * Now expressions such as `#eval do return 2`, where monad is unknown, work. It tries unifying the monad with `CommandElabM`, `TermElabM`, or `IO`.
+  * The classes `Lean.Eval` and `Lean.MetaEval` have been removed. These each used to be responsible for adapting monads and printing results. Now the `MonadEval` class is responsible for adapting monads for evaluation (it is similar to `MonadLift`, but instances are allowed to use default data when initializing state), and representing results is handled through a separate process.
+  * Error messages about failed instance synthesis are now more precise. Once it detects that a `MonadEval` class applies, then the error message will be specific about missing `ToExpr`/`Repr`/`ToString` instances.
+  * Fixes bugs where evaluating `MetaM` and `CoreM` wouldn't collect log messages.
+  * Fixes a bug where `let rec` could not be used in `#eval`.
+
+* `partial` definitions
+  * [#5780](https://github.com/leanprover/lean4/pull/5780) improves the error message when `partial` fails to prove a type is inhabited. Add delta deriving.
+  * [#5821](https://github.com/leanprover/lean4/pull/5821) gives `partial` inhabitation the ability to create local `Inhabited` instances from parameters.
+
+* **New tactic configuration syntax.** The configuration syntax for all core tactics has been given an upgrade. Rather than `simp (config := { contextual := true, maxSteps := 22})`, one can now write `simp +contextual (maxSteps := 22)`. Tactic authors can migrate by switching from `(config)?` to `optConfig` in tactic syntaxes and potentially deleting `mkOptionalNode` in elaborators. [#5883](https://github.com/leanprover/lean4/pull/5883), [#5898](https://github.com/leanprover/lean4/pull/5898),  [#5928](https://github.com/leanprover/lean4/pull/5928), and [#5932](https://github.com/leanprover/lean4/pull/5932). (Tactic authors, see breaking changes.)
+
+* `simp` tactic
+  * [#5632](https://github.com/leanprover/lean4/pull/5632) fixes the simpproc for `Fin` literals to reduce more consistently.
+  * [#5648](https://github.com/leanprover/lean4/pull/5648) fixes a bug in `simpa ... using t` where metavariables in `t` were not properly accounted for, and also improves the type mismatch error.
+  * [#5838](https://github.com/leanprover/lean4/pull/5838) fixes the docstring of `simp!` to actually talk about `simp!`.
+  * [#5870](https://github.com/leanprover/lean4/pull/5870) adds support for `attribute [simp ←]` (note the reverse direction). This adds the reverse of a theorem as a global simp theorem.
+
+* `decide` tactic
+  * [#5665](https://github.com/leanprover/lean4/pull/5665) adds `decide!` tactic for using kernel reduction (warning: this is renamed to `decide +kernel` in a future release).
+
+* `bv_decide` tactic
+  * [#5714](https://github.com/leanprover/lean4/pull/5714) adds inequality regression tests (@alexkeizer).
+  * [#5608](https://github.com/leanprover/lean4/pull/5608) adds `bv_toNat` tag for `toNat_ofInt` (@bollu).
+  * [#5618](https://github.com/leanprover/lean4/pull/5618) adds support for `at` in `ac_nf` and uses it in `bv_normalize` (@tobiasgrosser).
+  * [#5628](https://github.com/leanprover/lean4/pull/5628) adds udiv support.
+  * [#5635](https://github.com/leanprover/lean4/pull/5635) adds auxiliary bitblasters for negation and subtraction.
+  * [#5637](https://github.com/leanprover/lean4/pull/5637) adds more `getLsbD` bitblaster theory.
+  * [#5652](https://github.com/leanprover/lean4/pull/5652) adds umod support.
+  * [#5653](https://github.com/leanprover/lean4/pull/5653) adds performance benchmark for modulo.
+  * [#5655](https://github.com/leanprover/lean4/pull/5655) reduces error on `bv_check` to warning.
+  * [#5670](https://github.com/leanprover/lean4/pull/5670) adds `~~~(-x)` support.
+  * [#5673](https://github.com/leanprover/lean4/pull/5673) disables `ac_nf` by default.
+  * [#5675](https://github.com/leanprover/lean4/pull/5675) fixes context tracking in `bv_decide` counter example.
+  * [#5676](https://github.com/leanprover/lean4/pull/5676) adds an error when the LRAT proof is invalid.
+  * [#5781](https://github.com/leanprover/lean4/pull/5781) introduces uninterpreted symbols everywhere.
+  * [#5823](https://github.com/leanprover/lean4/pull/5823) adds `BitVec.sdiv` support.
+  * [#5852](https://github.com/leanprover/lean4/pull/5852) adds `BitVec.ofBool` support.
+  * [#5855](https://github.com/leanprover/lean4/pull/5855) adds `if` support.
+  * [#5869](https://github.com/leanprover/lean4/pull/5869) adds support for all the SMTLIB BitVec divison/remainder operations.
+  * [#5886](https://github.com/leanprover/lean4/pull/5886) adds embedded constraint substitution.
+  * [#5918](https://github.com/leanprover/lean4/pull/5918) fixes loose mvars bug in `bv_normalize`.
+  * Documentation:
+    * [#5636](https://github.com/leanprover/lean4/pull/5636) adds remarks about multiplication.
+
+* `conv` mode
+  * [#5861](https://github.com/leanprover/lean4/pull/5861) improves the `congr` conv tactic to handle "over-applied" functions.
+  * [#5894](https://github.com/leanprover/lean4/pull/5894) improves the `arg` conv tactic so that it can access more arguments and so that it can handle "over-applied" functions (it generates a specialized congruence lemma for the specific argument in question). Makes `arg 1` and `arg 2` apply to pi types in more situations. Adds negative indexing, for example `arg -2` is equivalent to the `lhs` tactic. Makes the `enter [...]` tactic show intermediate states like `rw`.
+
+* **Other tactics**
+  * [#4846](https://github.com/leanprover/lean4/pull/4846) fixes a bug where `generalize ... at *` would apply to implementation details (@ymherklotz).
+  * [#5730](https://github.com/leanprover/lean4/pull/5730) upstreams the `classical` tactic combinator.
+  * [#5815](https://github.com/leanprover/lean4/pull/5815) improves the error message when trying to unfold a local hypothesis that is not a local definition.
+  * [#5862](https://github.com/leanprover/lean4/pull/5862) and [#5863](https://github.com/leanprover/lean4/pull/5863) change how `apply` and `simp` elaborate, making them not disable error recovery. This improves hovers and completions when the term has elaboration errors.
+
+* `deriving` clauses
+  * [#5899](https://github.com/leanprover/lean4/pull/5899) adds declaration ranges for delta-derived instances.
+  * [#5265](https://github.com/leanprover/lean4/pull/5265) removes unused syntax in `deriving` clauses for providing arguments to deriving handlers (see breaking changes).
+
+* [#5065](https://github.com/leanprover/lean4/pull/5065) upstreams and updates `#where`, a command that reports the current scope information.
+
+* **Linters**
+  * [#5338](https://github.com/leanprover/lean4/pull/5338) makes the unused variables linter ignore variables defined in tactics by default now, avoiding performance bottlenecks.
+  * [#5644](https://github.com/leanprover/lean4/pull/5644) ensures that linters in general do not run on `#guard_msgs` itself.
+
+* **Metaprogramming interface**
+  * [#5720](https://github.com/leanprover/lean4/pull/5720) adds `pushGoal`/`pushGoals` and `popGoal` for manipulating the goal state. These are an alternative to `replaceMainGoal` and `getMainGoal`, and with them you don't need to worry about making sure nothing clears assigned metavariables from the goal list between assigning the main goal and using `replaceMainGoal`. Modifies `closeMainGoalUsing`, which is like a `TacticM` version of `liftMetaTactic`. Now the callback is run in a context where the main goal is removed from the goal list, and the callback is free to modify the goal list. Furthermore, the `checkUnassigned` argument has been replaced with `checkNewUnassigned`, which checks whether the value assigned to the goal has any *new* metavariables, relative to the start of execution of the callback. Modifies `withCollectingNewGoalsFrom` to take the `parentTag` argument explicitly rather than indirectly via `getMainTag`. Modifies `elabTermWithHoles` to optionally take `parentTag?`.
+  * [#5563](https://github.com/leanprover/lean4/pull/5563) fixes `getFunInfo` and `inferType` to use `withAtLeastTransparency` rather than `withTransparency`.
+  * [#5679](https://github.com/leanprover/lean4/pull/5679) fixes `RecursorVal.getInduct` to return the name of major argument’s type. This makes "structure eta" work for nested inductives.
+  * [#5681](https://github.com/leanprover/lean4/pull/5681) removes unused `mkRecursorInfoForKernelRec`.
+  * [#5686](https://github.com/leanprover/lean4/pull/5686) makes discrimination trees index the domains of foralls, for better performance of the simplify and type class search.
+  * [#5760](https://github.com/leanprover/lean4/pull/5760) adds `Lean.Expr.name?` recognizer for `Name` expressions.
+  * [#5800](https://github.com/leanprover/lean4/pull/5800) modifies `liftCommandElabM` to preserve more state, fixing an issue where using it would drop messages.
+  * [#5857](https://github.com/leanprover/lean4/pull/5857) makes it possible to use dot notation in `m!` strings, for example `m!"{.ofConstName n}"`.
+  * [#5841](https://github.com/leanprover/lean4/pull/5841) and [#5853](https://github.com/leanprover/lean4/pull/5853) record the complete list of `structure` parents in the `StructureInfo` environment extension.
+
+* **Other fixes or improvements**
+  * [#5566](https://github.com/leanprover/lean4/pull/5566) fixes a bug introduced in [#4781](https://github.com/leanprover/lean4/pull/4781) where heartbeat exceptions were no longer being handled properly. Now such exceptions are tagged with `runtime.maxHeartbeats` (@eric-wieser).
+  * [#5708](https://github.com/leanprover/lean4/pull/5708) modifies the proof objects produced by the proof-by-reflection tactics `ac_nf0` and `simp_arith` so that the kernel is less prone to reducing expensive atoms.
+  * [#5768](https://github.com/leanprover/lean4/pull/5768) adds a `#version` command that prints Lean's version information.
+  * [#5822](https://github.com/leanprover/lean4/pull/5822) fixes elaborator algorithms to match kernel algorithms for primitive projections (`Expr.proj`).
+  * [#5811](https://github.com/leanprover/lean4/pull/5811) improves the docstring for the `rwa` tactic.
+
+
+### Language server, widgets, and IDE extensions
+
+* [#5224](https://github.com/leanprover/lean4/pull/5224) fixes `WorkspaceClientCapabilities` to make `applyEdit` optional, in accordance with the LSP specification (@pzread).
+* [#5340](https://github.com/leanprover/lean4/pull/5340) fixes a server deadlock when shutting down the language server and a desync between client and language server after a file worker crash.
+* [#5560](https://github.com/leanprover/lean4/pull/5560) makes `initialize` and `builtin_initialize` participate in the call hierarchy and other requests.
+* [#5650](https://github.com/leanprover/lean4/pull/5650) makes references in attributes participate in the call hierarchy and other requests.
+* [#5666](https://github.com/leanprover/lean4/pull/5666) add auto-completion in tactic blocks without having to type the first character of the tactic, and adds tactic completion docs to tactic auto-completion items.
+* [#5677](https://github.com/leanprover/lean4/pull/5677) fixes several cases where goal states were not displayed in certain text cursor positions.
+* [#5707](https://github.com/leanprover/lean4/pull/5707) indicates deprecations in auto-completion items.
+* [#5736](https://github.com/leanprover/lean4/pull/5736), [#5752](https://github.com/leanprover/lean4/pull/5752), [#5763](https://github.com/leanprover/lean4/pull/5763), [#5802](https://github.com/leanprover/lean4/pull/5802), and [#5805](https://github.com/leanprover/lean4/pull/5805) fix various performance issues in the language server.
+* [#5801](https://github.com/leanprover/lean4/pull/5801) distinguishes theorem auto-completions from non-theorem auto-completions.
+
+### Pretty printing
+
+* [#5640](https://github.com/leanprover/lean4/pull/5640) fixes a bug where goal states in messages might print newlines as spaces.
+* [#5643](https://github.com/leanprover/lean4/pull/5643) adds option `pp.mvars.delayed` (default false), which when false causes delayed assignment metavariables to pretty print with what they are assigned to. Now `fun x : Nat => ?a` pretty prints as `fun x : Nat => ?a` rather than `fun x ↦ ?m.7 x`.
+* [#5711](https://github.com/leanprover/lean4/pull/5711) adds options `pp.mvars.anonymous` and `pp.mvars.levels`, which when false respectively cause expression metavariables and level metavariables to pretty print as `?_`.
+* [#5710](https://github.com/leanprover/lean4/pull/5710) adjusts the `⋯` elaboration warning to mention `pp.maxSteps`.
+
+* [#5759](https://github.com/leanprover/lean4/pull/5759) fixes the app unexpander for `sorryAx`.
+* [#5827](https://github.com/leanprover/lean4/pull/5827) improves accuracy of binder names in the signature pretty printer (like in output of `#check`). Also fixes the issue where consecutive hygienic names pretty print without a space separating them, so we now have `(x✝ y✝ : Nat)` rather than `(x✝y✝ : Nat)`.
+* [#5830](https://github.com/leanprover/lean4/pull/5830) makes sure all the core delaborators respond to `pp.explicit` when appropriate.
+* [#5639](https://github.com/leanprover/lean4/pull/5639) makes sure name literals use escaping when pretty printing.
+* [#5854](https://github.com/leanprover/lean4/pull/5854) adds delaborators for `<|>`, `<*>`, `>>`, `<*`, and `*>`.
+
+### Library
+
+* `Array`
+  * [#5687](https://github.com/leanprover/lean4/pull/5687) deprecates `Array.data`.
+  * [#5705](https://github.com/leanprover/lean4/pull/5705) uses a better default value for `Array.swapAt!`.
+  * [#5748](https://github.com/leanprover/lean4/pull/5748) moves `Array.mapIdx` lemmas to a new file.
+  * [#5749](https://github.com/leanprover/lean4/pull/5749) simplifies signature of `Array.mapIdx`.
+  * [#5758](https://github.com/leanprover/lean4/pull/5758) upstreams `Array.reduceOption`.
+  * [#5786](https://github.com/leanprover/lean4/pull/5786) adds simp lemmas for `Array.isEqv` and `BEq`.
+  * [#5796](https://github.com/leanprover/lean4/pull/5796) renames `Array.shrink` to `Array.take`, and relates it to `List.take`.
+  * [#5798](https://github.com/leanprover/lean4/pull/5798) upstreams `List.modify`, adds lemmas, relates to `Array.modify`.
+  * [#5799](https://github.com/leanprover/lean4/pull/5799) relates `Array.forIn` and `List.forIn`.
+  * [#5833](https://github.com/leanprover/lean4/pull/5833) adds `Array.forIn'`, and relates to `List`.
+  * [#5848](https://github.com/leanprover/lean4/pull/5848) fixes deprecations in `Init.Data.Array.Basic` to not recommend the deprecated constant.
+  * [#5895](https://github.com/leanprover/lean4/pull/5895) adds `LawfulBEq (Array α) ↔ LawfulBEq α`.
+  * [#5896](https://github.com/leanprover/lean4/pull/5896) moves `@[simp]` from `back_eq_back?` to `back_push`.
+  * [#5897](https://github.com/leanprover/lean4/pull/5897) renames `Array.back` to `back!`.
+
+* `List`
+  * [#5605](https://github.com/leanprover/lean4/pull/5605) removes `List.redLength`.
+  * [#5696](https://github.com/leanprover/lean4/pull/5696) upstreams `List.mapIdx` and adds lemmas.
+  * [#5697](https://github.com/leanprover/lean4/pull/5697) upstreams `List.foldxM_map`.
+  * [#5701](https://github.com/leanprover/lean4/pull/5701) renames `List.join` to `List.flatten`.
+  * [#5703](https://github.com/leanprover/lean4/pull/5703) upstreams `List.sum`.
+  * [#5706](https://github.com/leanprover/lean4/pull/5706) marks `prefix_append_right_inj` as a simp lemma.
+  * [#5716](https://github.com/leanprover/lean4/pull/5716) fixes `List.drop_drop` addition order.
+  * [#5731](https://github.com/leanprover/lean4/pull/5731) renames `List.bind` and `Array.concatMap` to `flatMap`.
+  * [#5732](https://github.com/leanprover/lean4/pull/5732) renames `List.pure` to `List.singleton`.
+  * [#5742](https://github.com/leanprover/lean4/pull/5742) upstreams `ne_of_mem_of_not_mem`.
+  * [#5743](https://github.com/leanprover/lean4/pull/5743) upstreams `ne_of_apply_ne`.
+  * [#5816](https://github.com/leanprover/lean4/pull/5816) adds more `List.modify` lemmas.
+  * [#5879](https://github.com/leanprover/lean4/pull/5879) renames `List.groupBy` to `splitBy`.
+  * [#5913](https://github.com/leanprover/lean4/pull/5913) relates `for` loops over `List` with `foldlM`.
+
+* `Nat`
+  * [#5694](https://github.com/leanprover/lean4/pull/5694) removes `instBEqNat`, which is redundant with `instBEqOfDecidableEq` but not defeq.
+  * [#5746](https://github.com/leanprover/lean4/pull/5746) deprecates `Nat.sum`.
+  * [#5785](https://github.com/leanprover/lean4/pull/5785) adds `Nat.forall_lt_succ` and variants.
+
+* Fixed width integers
+  * [#5323](https://github.com/leanprover/lean4/pull/5323) redefine unsigned fixed width integers in terms of `BitVec`.
+  * [#5735](https://github.com/leanprover/lean4/pull/5735) adds `UIntX.[val_ofNat, toBitVec_ofNat]`.
+  * [#5790](https://github.com/leanprover/lean4/pull/5790) defines `Int8`.
+  * [#5901](https://github.com/leanprover/lean4/pull/5901) removes native code for `UInt8.modn`.
+
+* `BitVec`
+  * [#5604](https://github.com/leanprover/lean4/pull/5604) completes `BitVec.[getMsbD|getLsbD|msb]` for shifts (@luisacicolini).
+  * [#5609](https://github.com/leanprover/lean4/pull/5609) adds lemmas for division when denominator is zero (@bollu).
+  * [#5620](https://github.com/leanprover/lean4/pull/5620) documents Bitblasting (@bollu)
+  * [#5623](https://github.com/leanprover/lean4/pull/5623) moves `BitVec.udiv/umod/sdiv/smod` after `add/sub/mul/lt` (@tobiasgrosser).
+  * [#5645](https://github.com/leanprover/lean4/pull/5645) defines `udiv` normal form to be `/`, resp. `umod` and `%` (@bollu).
+  * [#5646](https://github.com/leanprover/lean4/pull/5646) adds lemmas about arithmetic inequalities (@bollu).
+  * [#5680](https://github.com/leanprover/lean4/pull/5680) expands relationship with `toFin` (@tobiasgrosser).
+  * [#5691](https://github.com/leanprover/lean4/pull/5691) adds `BitVec.(getMSbD, msb)_(add, sub)` and `BitVec.getLsbD_sub` (@luisacicolini).
+  * [#5712](https://github.com/leanprover/lean4/pull/5712) adds `BitVec.[udiv|umod]_[zero|one|self]` (@tobiasgrosser).
+  * [#5718](https://github.com/leanprover/lean4/pull/5718) adds `BitVec.sdiv_[zero|one|self]` (@tobiasgrosser).
+  * [#5721](https://github.com/leanprover/lean4/pull/5721) adds `BitVec.(msb, getMsbD, getLsbD)_(neg, abs)` (@luisacicolini).
+  * [#5772](https://github.com/leanprover/lean4/pull/5772) adds `BitVec.toInt_sub`, simplifies `BitVec.toInt_neg` (@tobiasgrosser).
+  * [#5778](https://github.com/leanprover/lean4/pull/5778) prove that `intMin` the smallest signed bitvector (@alexkeizer).
+  * [#5851](https://github.com/leanprover/lean4/pull/5851) adds `(msb, getMsbD)_twoPow` (@luisacicolini).
+  * [#5858](https://github.com/leanprover/lean4/pull/5858) adds `BitVec.[zero_ushiftRight|zero_sshiftRight|zero_mul]` and cleans up BVDecide (@tobiasgrosser).
+  * [#5865](https://github.com/leanprover/lean4/pull/5865) adds `BitVec.(msb, getMsbD)_concat` (@luisacicolini).
+  * [#5881](https://github.com/leanprover/lean4/pull/5881) adds `Hashable (BitVec n)`
+
+* `String`/`Char`
+  * [#5728](https://github.com/leanprover/lean4/pull/5728) upstreams `String.dropPrefix?`.
+  * [#5745](https://github.com/leanprover/lean4/pull/5745) changes `String.dropPrefix?` signature.
+  * [#5747](https://github.com/leanprover/lean4/pull/5747) adds `Hashable Char` instance
+
+* `HashMap`
+  * [#5880](https://github.com/leanprover/lean4/pull/5880) adds interim implementation of `HashMap.modify`/`alter`
+
+* **Other**
+  * [#5704](https://github.com/leanprover/lean4/pull/5704) removes `@[simp]` from `Option.isSome_eq_isSome`.
+  * [#5739](https://github.com/leanprover/lean4/pull/5739) upstreams material on `Prod`.
+  * [#5740](https://github.com/leanprover/lean4/pull/5740) moves `Antisymm` to `Std.Antisymm`.
+  * [#5741](https://github.com/leanprover/lean4/pull/5741) upstreams basic material on `Sum`.
+  * [#5756](https://github.com/leanprover/lean4/pull/5756) adds `Nat.log2_two_pow` (@spinylobster).
+  * [#5892](https://github.com/leanprover/lean4/pull/5892) removes duplicated `ForIn` instances.
+  * [#5900](https://github.com/leanprover/lean4/pull/5900) removes `@[simp]` from `Sum.forall` and `Sum.exists`.
+  * [#5812](https://github.com/leanprover/lean4/pull/5812) removes redundant `Decidable` assumptions (@FR-vdash-bot).
+
+### Compiler, runtime, and FFI
+
+* [#5685](https://github.com/leanprover/lean4/pull/5685) fixes help message flags, removes the `-f` flag and adds the `-g` flag (@James-Oswald).
+* [#5930](https://github.com/leanprover/lean4/pull/5930) adds `--short-version` (`-V`) option to display short version (@juhp).
+* [#5144](https://github.com/leanprover/lean4/pull/5144) switches all 64-bit platforms over to consistently using GMP for bignum arithmetic.
+* [#5753](https://github.com/leanprover/lean4/pull/5753) raises the minimum supported Windows version to Windows 10 1903 (released May 2019).
+
+### Lake
+
+* [#5715](https://github.com/leanprover/lean4/pull/5715) changes `lake new math` to use `autoImplicit false` (@eric-wieser).
+* [#5688](https://github.com/leanprover/lean4/pull/5688) makes `Lake` not create core aliases in the `Lake` namespace.
+* [#5924](https://github.com/leanprover/lean4/pull/5924) adds a `text` option for `buildFile*` utilities.
+* [#5789](https://github.com/leanprover/lean4/pull/5789) makes `lake init` not `git init` when inside git work tree (@haoxins).
+* [#5684](https://github.com/leanprover/lean4/pull/5684) has Lake update a package's `lean-toolchain` file on `lake update` if it finds the package's direct dependencies use a newer compatible toolchain. To skip this step, use the `--keep-toolchain` CLI option. (See breaking changes.)
+* [#6218](https://github.com/leanprover/lean4/pull/6218) makes Lake no longer automatically fetch GitHub cloud releases if the package build directory is already present (mirroring the behavior of the Reservoir cache). This prevents the cache from clobbering existing prebuilt artifacts. Users can still manually fetch the cache and clobber the build directory by running `lake build <pkg>:release`.
+* [#6231](https://github.com/leanprover/lean4/pull/6231) improves the errors Lake produces when it fails to fetch a dependency from Reservoir. If the package is not indexed, it will produce a suggestion about how to require it from GitHub.
+
+### Documentation
+
+* [#5617](https://github.com/leanprover/lean4/pull/5617) fixes MSYS2 build instructions.
+* [#5725](https://github.com/leanprover/lean4/pull/5725) points out that `OfScientific` is called with raw literals (@eric-wieser).
+* [#5794](https://github.com/leanprover/lean4/pull/5794) adds a stub for application ellipsis notation (@eric-wieser).
+
+### Breaking changes
+
+* The syntax for providing arguments to deriving handlers has been removed, which was not used by any major Lean projects in the ecosystem. As a result, the  `applyDerivingHandlers` now takes one fewer argument, `registerDerivingHandlerWithArgs` is now simply `registerDerivingHandler`, `DerivingHandler` no longer includes the unused parameter, and `DerivingHandlerNoArgs` has been deprecated. To migrate code, delete the unused `none` argument and use `registerDerivingHandler` and `DerivingHandler`. ([#5265](https://github.com/leanprover/lean4/pull/5265))
+* The minimum supported Windows version has been raised to Windows 10 1903, released May 2019. ([#5753](https://github.com/leanprover/lean4/pull/5753))
+* The `--lean` CLI option for `lake` was removed. Use the `LEAN` environment variable instead. ([#5684](https://github.com/leanprover/lean4/pull/5684))
+* The `inductive ... :=`, `structure ... :=`, and `class ... :=` syntaxes have been deprecated in favor of the `... where` variants. The old syntax produces a warning, controlled by the `linter.deprecated` option. ([#5542](https://github.com/leanprover/lean4/pull/5542))
+* The generated tactic configuration elaborators now land in `TacticM` to make use of the current recovery state. Commands that wish to elaborate configurations should now use `declare_command_config_elab` instead of `declare_config_elab` to get an elaborator landing in `CommandElabM`. Syntaxes should migrate to `optConfig` instead of `(config)?`, but the elaborators are reverse compatible. ([#5883](https://github.com/leanprover/lean4/pull/5883))
+
 
 v4.13.0
 ----------

doc/lexical_structure.md

@@ -128,16 +128,16 @@ Numeric literals can be specified in various bases.
 
 ```
    numeral    : numeral10 | numeral2 | numeral8 | numeral16
-   numeral10  : [0-9]+
-   numeral2   : "0" [bB] [0-1]+
-   numeral8   : "0" [oO] [0-7]+
-   numeral16  : "0" [xX] hex_char+
+   numeral10  : [0-9]+ ("_"+ [0-9]+)*
+   numeral2   : "0" [bB] ("_"* [0-1]+)+
+   numeral8   : "0" [oO] ("_"* [0-7]+)+
+   numeral16  : "0" [xX] ("_"* hex_char+)+
 ```
 
 Floating point literals are also possible with optional exponent:
 
 ```
-   float    : [0-9]+ "." [0-9]+ [[eE[+-][0-9]+]
+   float    : numeral10 "." numeral10? [eE[+-]numeral10]
 ```
 
 For example:
@@ -147,6 +147,7 @@ constant w : Int := 55
 constant x : Nat := 26085
 constant y : Nat := 0x65E5
 constant z : Float := 2.548123e-05
+constant b : Bool := 0b_11_01_10_00
 ```
 
 Note: that negative numbers are created by applying the "-" negation prefix operator to the number, for example:

src/Init/Data.lean

@@ -21,6 +21,7 @@ import Init.Data.Fin
 import Init.Data.UInt
 import Init.Data.SInt
 import Init.Data.Float
+import Init.Data.Float32
 import Init.Data.Option
 import Init.Data.Ord
 import Init.Data.Random

src/Init/Data/Array/Basic.lean

@@ -11,7 +11,7 @@ import Init.Data.UInt.BasicAux
 import Init.Data.Repr
 import Init.Data.ToString.Basic
 import Init.GetElem
-import Init.Data.List.ToArray
+import Init.Data.List.ToArrayImpl
 import Init.Data.Array.Set
 
 universe u v w
@@ -85,6 +85,8 @@ theorem ext' {as bs : Array α} (h : as.toList = bs.toList) : as = bs := by
 
 @[simp] theorem getElem_toList {a : Array α} {i : Nat} (h : i < a.size) : a.toList[i] = a[i] := rfl
 
+@[simp] theorem getElem?_toList {a : Array α} {i : Nat} : a.toList[i]? = a[i]? := rfl
+
 /-- `a ∈ as` is a predicate which asserts that `a` is in the array `as`. -/
 -- NB: This is defined as a structure rather than a plain def so that a lemma
 -- like `sizeOf_lt_of_mem` will not apply with no actual arrays around.
@@ -97,6 +99,9 @@ instance : Membership α (Array α) where
 theorem mem_def {a : α} {as : Array α} : a ∈ as ↔ a ∈ as.toList :=
   ⟨fun | .mk h => h, Array.Mem.mk⟩
 
+@[simp] theorem mem_toArray {a : α} {l : List α} : a ∈ l.toArray ↔ a ∈ l := by
+  simp [mem_def]
+
 @[simp] theorem getElem_mem {l : Array α} {i : Nat} (h : i < l.size) : l[i] ∈ l := by
   rw [Array.mem_def, ← getElem_toList]
   apply List.getElem_mem
@@ -242,7 +247,7 @@ def singleton (v : α) : Array α :=
   mkArray 1 v
 
 def back! [Inhabited α] (a : Array α) : α :=
-  a.get! (a.size - 1)
+  a[a.size - 1]!
 
 @[deprecated back! (since := "2024-10-31")] abbrev back := @back!
 
@@ -658,7 +663,7 @@ def all (as : Array α) (p : α → Bool) (start := 0) (stop := as.size) : Bool
   Id.run <| as.allM p start stop
 
 def contains [BEq α] (as : Array α) (a : α) : Bool :=
-  as.any (· == a)
+  as.any (a == ·)
 
 def elem [BEq α] (a : α) (as : Array α) : Bool :=
   as.contains a

src/Init/Data/Array/Find.lean

@@ -81,7 +81,7 @@ theorem getElem_zero_flatten.proof {L : Array (Array α)} (h : 0 < L.flatten.siz
     (L.findSome? fun l => l[0]?).isSome := by
   cases L using array_array_induction
   simp only [List.findSome?_toArray, List.findSome?_map, Function.comp_def, List.getElem?_toArray,
-    List.findSome?_isSome_iff, List.isSome_getElem?]
+    List.findSome?_isSome_iff, isSome_getElem?]
   simp only [flatten_toArray_map_toArray, size_toArray, List.length_flatten,
     Nat.sum_pos_iff_exists_pos, List.mem_map] at h
   obtain ⟨_, ⟨xs, m, rfl⟩, h⟩ := h

src/Init/Data/Array/TakeDrop.lean

@@ -12,7 +12,7 @@ namespace Array
 theorem exists_of_uset (self : Array α) (i d h) :
     ∃ l₁ l₂, self.toList = l₁ ++ self[i] :: l₂ ∧ List.length l₁ = i.toNat ∧
       (self.uset i d h).toList = l₁ ++ d :: l₂ := by
-  simpa only [ugetElem_eq_getElem, getElem_eq_getElem_toList, uset, toList_set] using
+  simpa only [ugetElem_eq_getElem, ← getElem_toList, uset, toList_set] using
     List.exists_of_set _
 
 end Array

src/Init/Data/BEq.lean

@@ -40,6 +40,9 @@ theorem BEq.symm [BEq α] [PartialEquivBEq α] {a b : α} : a == b → b == a :=
 theorem BEq.comm [BEq α] [PartialEquivBEq α] {a b : α} : (a == b) = (b == a) :=
   Bool.eq_iff_iff.2 ⟨BEq.symm, BEq.symm⟩
 
+theorem bne_comm [BEq α] [PartialEquivBEq α] {a b : α} : (a != b) = (b != a) := by
+  rw [bne, BEq.comm, bne]
+
 theorem BEq.symm_false [BEq α] [PartialEquivBEq α] {a b : α} : (a == b) = false → (b == a) = false :=
   BEq.comm (α := α) ▸ id
 

src/Init/Data/BitVec/Bitblast.lean

@@ -462,7 +462,7 @@ theorem msb_neg {w : Nat} {x : BitVec w} :
       case true =>
         apply hmin
         apply eq_of_getMsbD_eq
-        rintro ⟨i, hi⟩
+        intro i hi
         simp only [getMsbD_intMin, w_pos, decide_true, Bool.true_and]
         cases i
         case zero => exact hmsb
@@ -470,7 +470,7 @@ theorem msb_neg {w : Nat} {x : BitVec w} :
       case false =>
         apply hzero
         apply eq_of_getMsbD_eq
-        rintro ⟨i, hi⟩
+        intro i hi
         simp only [getMsbD_zero]
         cases i
         case zero => exact hmsb
@@ -573,11 +573,11 @@ theorem setWidth_setWidth_succ_eq_setWidth_setWidth_add_twoPow (x : BitVec w) (i
     setWidth w (x.setWidth (i + 1)) =
       setWidth w (x.setWidth i) + (x &&& twoPow w i) := by
   rw [add_eq_or_of_and_eq_zero]
-  · ext k
-    simp only [getLsbD_setWidth, Fin.is_lt, decide_true, Bool.true_and, getLsbD_or, getLsbD_and]
+  · ext k h
+    simp only [getLsbD_setWidth, h, decide_true, Bool.true_and, getLsbD_or, getLsbD_and]
     by_cases hik : i = k
     · subst hik
-      simp
+      simp [h]
     · simp only [getLsbD_twoPow, hik, decide_false, Bool.and_false, Bool.or_false]
       by_cases hik' : k < (i + 1)
       · have hik'' : k < i := by omega

src/Init/Data/BitVec/Lemmas.lean

@@ -173,21 +173,21 @@ theorem getMsbD_eq_getMsb?_getD (x : BitVec w) (i : Nat) :
 -- We choose `eq_of_getLsbD_eq` as the `@[ext]` theorem for `BitVec`
 -- somewhat arbitrarily over `eq_of_getMsbD_eq`.
 @[ext] theorem eq_of_getLsbD_eq {x y : BitVec w}
-    (pred : ∀(i : Fin w), x.getLsbD i.val = y.getLsbD i.val) : x = y := by
+    (pred : ∀ i, i < w → x.getLsbD i = y.getLsbD i) : x = y := by
   apply eq_of_toNat_eq
   apply Nat.eq_of_testBit_eq
   intro i
   if i_lt : i < w then
-    exact pred ⟨i, i_lt⟩
+    exact pred i i_lt
   else
     have p : i ≥ w := Nat.le_of_not_gt i_lt
     simp [testBit_toNat, getLsbD_ge _ _ p]
 
 theorem eq_of_getMsbD_eq {x y : BitVec w}
-    (pred : ∀(i : Fin w), x.getMsbD i.val = y.getMsbD i.val) : x = y := by
+    (pred : ∀ i, i < w → x.getMsbD i = y.getMsbD i) : x = y := by
   simp only [getMsbD] at pred
   apply eq_of_getLsbD_eq
-  intro ⟨i, i_lt⟩
+  intro i i_lt
   if w_zero : w = 0 then
     simp [w_zero]
   else
@@ -199,7 +199,7 @@ theorem eq_of_getMsbD_eq {x y : BitVec w}
       simp only [Nat.sub_sub]
       apply Nat.sub_lt w_pos
       simp [Nat.succ_add]
-    have q := pred ⟨w - 1 - i, q_lt⟩
+    have q := pred (w - 1 - i) q_lt
     simpa [q_lt, Nat.sub_sub_self, r] using q
 
 -- This cannot be a `@[simp]` lemma, as it would be tried at every term.
@@ -241,8 +241,11 @@ theorem toFin_one  : toFin (1 : BitVec w) = 1 := by
 @[simp] theorem toNat_ofBool (b : Bool) : (ofBool b).toNat = b.toNat := by
   cases b <;> rfl
 
-@[simp] theorem msb_ofBool (b : Bool) : (ofBool b).msb = b := by
-  cases b <;> simp [BitVec.msb, getMsbD, getLsbD]
+@[simp] theorem toInt_ofBool (b : Bool) : (ofBool b).toInt = -b.toInt := by
+  cases b <;> rfl
+
+@[simp] theorem toFin_ofBool (b : Bool) : (ofBool b).toFin = Fin.ofNat' 2 (b.toNat) := by
+  cases b <;> rfl
 
 theorem ofNat_one (n : Nat) : BitVec.ofNat 1 n = BitVec.ofBool (n % 2 = 1) :=  by
   rcases (Nat.mod_two_eq_zero_or_one n) with h | h <;> simp [h, BitVec.ofNat, Fin.ofNat']
@@ -366,6 +369,12 @@ theorem getElem_ofBool {b : Bool} {i : Nat} : (ofBool b)[0] = b := by
   · simp only [ofBool]
     by_cases hi : i = 0 <;> simp [hi] <;> omega
 
+@[simp] theorem getMsbD_ofBool (b : Bool) : (ofBool b).getMsbD i = (decide (i = 0) && b) := by
+  cases b <;> simp [getMsbD]
+
+@[simp] theorem msb_ofBool (b : Bool) : (ofBool b).msb = b := by
+  cases b <;> simp [BitVec.msb]
+
 /-! ### msb -/
 
 @[simp] theorem msb_zero : (0#w).msb = false := by simp [BitVec.msb, getMsbD]
@@ -498,6 +507,9 @@ theorem toInt_ofNat {n : Nat} (x : Nat) :
 @[simp] theorem ofInt_ofNat (w n : Nat) :
   BitVec.ofInt w (no_index (OfNat.ofNat n)) = BitVec.ofNat w (OfNat.ofNat n) := rfl
 
+@[simp] theorem ofInt_toInt {x : BitVec w} : BitVec.ofInt w x.toInt = x := by
+  by_cases h : 2 * x.toNat < 2^w <;> ext <;> simp [getLsbD, h, BitVec.toInt]
+
 theorem toInt_neg_iff {w : Nat} {x : BitVec w} :
     BitVec.toInt x < 0 ↔ 2 ^ w ≤ 2 * x.toNat := by
   simp [toInt_eq_toNat_cond]; omega
@@ -569,6 +581,10 @@ theorem zeroExtend_eq_setWidth {v : Nat} {x : BitVec w} :
     (x.setWidth v).toInt = Int.bmod x.toNat (2^v) := by
   simp [toInt_eq_toNat_bmod, toNat_setWidth, Int.emod_bmod]
 
+@[simp] theorem toFin_setWidth {x : BitVec w} :
+    (x.setWidth v).toFin = Fin.ofNat' (2^v) x.toNat := by
+  ext; simp
+
 theorem setWidth'_eq {x : BitVec w} (h : w ≤ v) : x.setWidth' h = x.setWidth v := by
   apply eq_of_toNat_eq
   rw [toNat_setWidth, toNat_setWidth']
@@ -645,6 +661,20 @@ theorem getElem?_setWidth (m : Nat) (x : BitVec n) (i : Nat) :
     getLsbD (setWidth m x) i = (decide (i < m) && getLsbD x i) := by
   simp [getLsbD, toNat_setWidth, Nat.testBit_mod_two_pow]
 
+theorem getMsbD_setWidth {m : Nat} {x : BitVec n} {i : Nat} :
+    getMsbD (setWidth m x) i = (decide (m - n ≤ i) && getMsbD x (i + n - m)) := by
+  unfold setWidth
+  by_cases h : n ≤ m <;> simp only [h]
+  · by_cases h' : m - n ≤ i
+    <;> simp [h', show i - (m - n) = i + n - m by omega]
+  · simp only [show m - n = 0 by omega, getMsbD, getLsbD_setWidth]
+    by_cases h' : i < m
+    · simp [show m - 1 - i < m by omega, show i + n - m < n by omega,
+        show n - 1 - (i + n - m) = m - 1 - i by omega]
+      omega
+    · simp [h']
+      omega
+
 @[simp] theorem getMsbD_setWidth_add {x : BitVec w} (h : k ≤ i) :
     (x.setWidth (w + k)).getMsbD i = x.getMsbD (i - k) := by
   by_cases h : w = 0
@@ -689,14 +719,15 @@ theorem msb_setWidth'' (x : BitVec w) : (x.setWidth (k + 1)).msb = x.getLsbD k :
 /-- zero extending a bitvector to width 1 equals the boolean of the lsb. -/
 theorem setWidth_one_eq_ofBool_getLsb_zero (x : BitVec w) :
     x.setWidth 1 = BitVec.ofBool (x.getLsbD 0) := by
-  ext i
-  simp [getLsbD_setWidth, Fin.fin_one_eq_zero i]
+  ext i h
+  simp at h
+  simp [getLsbD_setWidth, h]
 
 /-- Zero extending `1#v` to `1#w` equals `1#w` when `v > 0`. -/
 theorem setWidth_ofNat_one_eq_ofNat_one_of_lt {v w : Nat} (hv : 0 < v) :
     (BitVec.ofNat v 1).setWidth w = BitVec.ofNat w 1 := by
-  ext ⟨i, hilt⟩
-  simp only [getLsbD_setWidth, hilt, decide_true, getLsbD_ofNat, Bool.true_and,
+  ext i h
+  simp only [getLsbD_setWidth, h, decide_true, getLsbD_ofNat, Bool.true_and,
     Bool.and_iff_right_iff_imp, decide_eq_true_eq]
   intros hi₁
   have hv := Nat.testBit_one_eq_true_iff_self_eq_zero.mp hi₁
@@ -723,8 +754,7 @@ protected theorem extractLsb_ofFin {n} (x : Fin (2^n)) (hi lo : Nat) :
 @[simp]
 protected theorem extractLsb_ofNat (x n : Nat) (hi lo : Nat) :
   extractLsb hi lo (BitVec.ofNat n x) = .ofNat (hi - lo + 1) ((x % 2^n) >>> lo) := by
-  apply eq_of_getLsbD_eq
-  intro ⟨i, _lt⟩
+  ext i
   simp [BitVec.ofNat]
 
 @[simp] theorem extractLsb'_toNat (s m : Nat) (x : BitVec n) :
@@ -811,8 +841,8 @@ theorem extractLsb'_eq_extractLsb {w : Nat} (x : BitVec w) (start len : Nat) (h
 
 @[simp] theorem setWidth_or {x y : BitVec w} :
     (x ||| y).setWidth k = x.setWidth k ||| y.setWidth k := by
-  ext
-  simp
+  ext i h
+  simp [h]
 
 theorem or_assoc (x y z : BitVec w) :
     x ||| y ||| z = x ||| (y ||| z) := by
@@ -845,12 +875,12 @@ instance : Std.LawfulCommIdentity (α := BitVec n) (· ||| · ) (0#n) where
   simp
 
 @[simp] theorem or_allOnes {x : BitVec w} : x ||| allOnes w = allOnes w := by
-  ext i
-  simp
+  ext i h
+  simp [h]
 
 @[simp] theorem allOnes_or {x : BitVec w} : allOnes w ||| x = allOnes w := by
-  ext i
-  simp
+  ext i h
+  simp [h]
 
 /-! ### and -/
 
@@ -884,8 +914,8 @@ instance : Std.LawfulCommIdentity (α := BitVec n) (· ||| · ) (0#n) where
 
 @[simp] theorem setWidth_and {x y : BitVec w} :
     (x &&& y).setWidth k = x.setWidth k &&& y.setWidth k := by
-  ext
-  simp
+  ext i h
+  simp [h]
 
 theorem and_assoc (x y z : BitVec w) :
     x &&& y &&& z = x &&& (y &&& z) := by
@@ -915,15 +945,15 @@ instance : Std.IdempotentOp (α := BitVec n) (· &&& · ) where
   simp
 
 @[simp] theorem and_allOnes {x : BitVec w} : x &&& allOnes w = x := by
-  ext i
-  simp
+  ext i h
+  simp [h]
 
 instance : Std.LawfulCommIdentity (α := BitVec n) (· &&& · ) (allOnes n) where
   right_id _ := BitVec.and_allOnes
 
 @[simp] theorem allOnes_and {x : BitVec w} : allOnes w &&& x = x := by
-  ext i
-  simp
+  ext i h
+  simp [h]
 
 /-! ### xor -/
 
@@ -960,8 +990,8 @@ instance : Std.LawfulCommIdentity (α := BitVec n) (· &&& · ) (allOnes n) wher
 
 @[simp] theorem setWidth_xor {x y : BitVec w} :
     (x ^^^ y).setWidth k = x.setWidth k ^^^ y.setWidth k := by
-  ext
-  simp
+  ext i h
+  simp [h]
 
 theorem xor_assoc (x y z : BitVec w) :
     x ^^^ y ^^^ z = x ^^^ (y ^^^ z) := by
@@ -1054,9 +1084,9 @@ theorem not_def {x : BitVec v} : ~~~x = allOnes v ^^^ x := rfl
   rw [Nat.testBit_two_pow_sub_succ x.isLt]
   simp [h]
 
-@[simp] theorem setWidth_not {x : BitVec w} (h : k ≤ w) :
+@[simp] theorem setWidth_not {x : BitVec w} (_ : k ≤ w) :
     (~~~x).setWidth k = ~~~(x.setWidth k) := by
-  ext
+  ext i h
   simp [h]
   omega
 
@@ -1069,17 +1099,17 @@ theorem not_def {x : BitVec v} : ~~~x = allOnes v ^^^ x := rfl
   simp
 
 @[simp] theorem xor_allOnes {x : BitVec w} : x ^^^ allOnes w = ~~~ x := by
-  ext i
-  simp
+  ext i h
+  simp [h]
 
 @[simp] theorem allOnes_xor {x : BitVec w} : allOnes w ^^^ x = ~~~ x := by
-  ext i
-  simp
+  ext i h
+  simp [h]
 
 @[simp]
 theorem not_not {b : BitVec w} : ~~~(~~~b) = b := by
-  ext i
-  simp
+  ext i h
+  simp [h]
 
 theorem not_eq_comm {x y : BitVec w} : ~~~ x = y ↔ x = ~~~ y := by
   constructor
@@ -1154,24 +1184,21 @@ theorem zero_shiftLeft (n : Nat) : 0#w <<< n = 0#w := by
 
 theorem shiftLeft_xor_distrib (x y : BitVec w) (n : Nat) :
     (x ^^^ y) <<< n = (x <<< n) ^^^ (y <<< n) := by
-  ext i
-  simp only [getLsbD_shiftLeft, Fin.is_lt, decide_true, Bool.true_and, getLsbD_xor]
-  by_cases h : i < n
-    <;> simp [h]
+  ext i h
+  simp only [getLsbD_shiftLeft, h, decide_true, Bool.true_and, getLsbD_xor]
+  by_cases h' : i < n <;> simp [h']
 
 theorem shiftLeft_and_distrib (x y : BitVec w) (n : Nat) :
     (x &&& y) <<< n = (x <<< n) &&& (y <<< n) := by
-  ext i
-  simp only [getLsbD_shiftLeft, Fin.is_lt, decide_true, Bool.true_and, getLsbD_and]
-  by_cases h : i < n
-    <;> simp [h]
+  ext i h
+  simp only [getLsbD_shiftLeft, h, decide_true, Bool.true_and, getLsbD_and]
+  by_cases h' : i < n <;> simp [h']
 
 theorem shiftLeft_or_distrib (x y : BitVec w) (n : Nat) :
     (x ||| y) <<< n = (x <<< n) ||| (y <<< n) := by
-  ext i
-  simp only [getLsbD_shiftLeft, Fin.is_lt, decide_true, Bool.true_and, getLsbD_or]
-  by_cases h : i < n
-    <;> simp [h]
+  ext i h
+  simp only [getLsbD_shiftLeft, h, decide_true, Bool.true_and, getLsbD_or]
+  by_cases h' : i < n <;> simp [h']
 
 @[simp] theorem getMsbD_shiftLeft (x : BitVec w) (i) :
     (x <<< i).getMsbD k = x.getMsbD (k + i) := by
@@ -1510,12 +1537,12 @@ theorem msb_sshiftRight {n : Nat} {x : BitVec w} :
     simp [show n = 0 by omega]
 
 @[simp] theorem sshiftRight_zero {x : BitVec w} : x.sshiftRight 0 = x := by
-  ext i
-  simp [getLsbD_sshiftRight]
+  ext i h
+  simp [getLsbD_sshiftRight, h]
 
 @[simp] theorem zero_sshiftRight {n : Nat} : (0#w).sshiftRight n = 0#w := by
-  ext i
-  simp [getLsbD_sshiftRight]
+  ext i h
+  simp [getLsbD_sshiftRight, h]
 
 theorem sshiftRight_add {x : BitVec w} {m n : Nat} :
     x.sshiftRight (m + n) = (x.sshiftRight m).sshiftRight n := by
@@ -1616,7 +1643,7 @@ private theorem Int.negSucc_emod (m : Nat) (n : Int) :
     -(m + 1) % n = Int.subNatNat (Int.natAbs n) ((m % Int.natAbs n) + 1) := rfl
 
 /-- The sign extension is the same as zero extending when `msb = false`. -/
-theorem signExtend_eq_not_setWidth_not_of_msb_false {x : BitVec w} {v : Nat} (hmsb : x.msb = false) :
+theorem signExtend_eq_setWidth_of_msb_false {x : BitVec w} {v : Nat} (hmsb : x.msb = false) :
     x.signExtend v = x.setWidth v := by
   ext i
   by_cases hv : i < v
@@ -1652,21 +1679,36 @@ theorem signExtend_eq_not_setWidth_not_of_msb_true {x : BitVec w} {v : Nat} (hms
 theorem getLsbD_signExtend (x  : BitVec w) {v i : Nat} :
     (x.signExtend v).getLsbD i = (decide (i < v) && if i < w then x.getLsbD i else x.msb) := by
   rcases hmsb : x.msb with rfl | rfl
-  · rw [signExtend_eq_not_setWidth_not_of_msb_false hmsb]
+  · rw [signExtend_eq_setWidth_of_msb_false hmsb]
     by_cases (i < v) <;> by_cases (i < w) <;> simp_all <;> omega
   · rw [signExtend_eq_not_setWidth_not_of_msb_true hmsb]
     by_cases (i < v) <;> by_cases (i < w) <;> simp_all <;> omega
 
+theorem getMsbD_signExtend {x : BitVec w} {v i : Nat} :
+    (x.signExtend v).getMsbD i =
+      (decide (i < v) && if v - w ≤ i then x.getMsbD (i + w - v) else x.msb) := by
+  rcases hmsb : x.msb with rfl | rfl
+  · simp only [signExtend_eq_setWidth_of_msb_false hmsb, getMsbD_setWidth]
+    by_cases h : v - w ≤ i <;> simp [h, getMsbD] <;> omega
+  · simp only [signExtend_eq_not_setWidth_not_of_msb_true hmsb, getMsbD_not, getMsbD_setWidth]
+    by_cases h : i < v <;> by_cases h' : v - w ≤ i <;> simp [h, h'] <;> omega
+
 theorem getElem_signExtend {x  : BitVec w} {v i : Nat} (h : i < v) :
     (x.signExtend v)[i] = if i < w then x.getLsbD i else x.msb := by
   rw [←getLsbD_eq_getElem, getLsbD_signExtend]
   simp [h]
 
+theorem msb_signExtend {x : BitVec w} :
+    (x.signExtend v).msb = (decide (0 < v) && if w ≥ v then x.getMsbD (w - v) else x.msb) := by
+  by_cases h : w ≥ v
+  · simp [h, BitVec.msb, getMsbD_signExtend, show v - w = 0 by omega]
+  · simp [h, BitVec.msb, getMsbD_signExtend, show ¬ (v - w = 0) by omega]
+
 /-- Sign extending to a width smaller than the starting width is a truncation. -/
 theorem signExtend_eq_setWidth_of_lt (x : BitVec w) {v : Nat} (hv : v ≤ w):
   x.signExtend v = x.setWidth v := by
-  ext i
-  simp only [getLsbD_signExtend, Fin.is_lt, decide_true, Bool.true_and, getLsbD_setWidth,
+  ext i h
+  simp only [getLsbD_signExtend, h, decide_true, Bool.true_and, getLsbD_setWidth,
     ite_eq_left_iff, Nat.not_lt]
   omega
 
@@ -1760,35 +1802,34 @@ theorem append_def (x : BitVec v) (y : BitVec w) :
   rfl
 
 theorem getLsbD_append {x : BitVec n} {y : BitVec m} :
-    getLsbD (x ++ y) i = bif i < m then getLsbD y i else getLsbD x (i - m) := by
+    getLsbD (x ++ y) i = if i < m then getLsbD y i else getLsbD x (i - m) := by
   simp only [append_def, getLsbD_or, getLsbD_shiftLeftZeroExtend, getLsbD_setWidth']
   by_cases h : i < m
   · simp [h]
   · simp_all [h]
 
 theorem getElem_append {x : BitVec n} {y : BitVec m} (h : i < n + m) :
-    (x ++ y)[i] = bif i < m then getLsbD y i else getLsbD x (i - m) := by
+    (x ++ y)[i] = if i < m then getLsbD y i else getLsbD x (i - m) := by
   simp only [append_def, getElem_or, getElem_shiftLeftZeroExtend, getElem_setWidth']
   by_cases h' : i < m
   · simp [h']
   · simp_all [h']
 
 @[simp] theorem getMsbD_append {x : BitVec n} {y : BitVec m} :
-    getMsbD (x ++ y) i = bif n ≤ i then getMsbD y (i - n) else getMsbD x i := by
+    getMsbD (x ++ y) i = if n ≤ i then getMsbD y (i - n) else getMsbD x i := by
   simp only [append_def]
   by_cases h : n ≤ i
   · simp [h]
   · simp [h]
 
 theorem msb_append {x : BitVec w} {y : BitVec v} :
-    (x ++ y).msb = bif (w == 0) then (y.msb) else (x.msb) := by
+    (x ++ y).msb = if w = 0 then y.msb else x.msb := by
   rw [← append_eq, append]
   simp only [msb_or, msb_shiftLeftZeroExtend, msb_setWidth']
   by_cases h : w = 0
   · subst h
     simp [BitVec.msb, getMsbD]
-  · rw [cond_eq_if]
-    have q : 0 < w + v := by omega
+  · have q : 0 < w + v := by omega
     have t : y.getLsbD (w + v - 1) = false := getLsbD_ge _ _ (by omega)
     simp [h, q, t, BitVec.msb, getMsbD]
 
@@ -1804,7 +1845,7 @@ theorem msb_append {x : BitVec w} {y : BitVec v} :
 
 @[simp] theorem zero_append_zero : 0#v ++ 0#w = 0#(v + w) := by
   ext
-  simp only [getLsbD_append, getLsbD_zero, Bool.cond_self]
+  simp only [getLsbD_append, getLsbD_zero, ite_self]
 
 @[simp] theorem cast_append_right (h : w + v = w + v') (x : BitVec w) (y : BitVec v) :
     (x ++ y).cast h = x ++ y.cast (by omega) := by
@@ -1824,21 +1865,19 @@ theorem msb_append {x : BitVec w} {y : BitVec v} :
 
 theorem setWidth_append {x : BitVec w} {y : BitVec v} :
     (x ++ y).setWidth k = if h : k ≤ v then y.setWidth k else (x.setWidth (k - v) ++ y).cast (by omega) := by
-  apply eq_of_getLsbD_eq
-  intro i
-  simp only [getLsbD_setWidth, Fin.is_lt, decide_true, getLsbD_append, Bool.true_and]
-  split
-  · have t : i < v := by omega
-    simp [t]
-  · by_cases t : i < v
-    · simp [t, getLsbD_append]
-    · have t' : i - v < k - v := by omega
-      simp [t, t', getLsbD_append]
+  ext i h
+  simp only [getLsbD_setWidth, h, getLsbD_append]
+  split <;> rename_i h₁ <;> split <;> rename_i h₂
+  · simp [h]
+  · simp [getLsbD_append, h₁]
+  · omega
+  · simp [getLsbD_append, h₁]
+    omega
 
 @[simp] theorem setWidth_append_of_eq {x : BitVec v} {y : BitVec w} (h : w' = w) : setWidth (v' + w') (x ++ y) = setWidth v' x ++ setWidth w' y := by
   subst h
-  ext i
-  simp only [getLsbD_setWidth, Fin.is_lt, decide_true, getLsbD_append, cond_eq_if,
+  ext i h
+  simp only [getLsbD_setWidth, h, decide_true, getLsbD_append, cond_eq_if,
     decide_eq_true_eq, Bool.true_and, setWidth_eq]
   split
   · simp_all
@@ -1888,12 +1927,12 @@ theorem shiftLeft_ushiftRight {x : BitVec w} {n : Nat}:
   case succ n ih =>
     rw [BitVec.shiftLeft_add, Nat.add_comm, BitVec.shiftRight_add, ih,
        Nat.add_comm, BitVec.shiftLeft_add, BitVec.shiftLeft_and_distrib]
-    ext i
+    ext i h
     by_cases hw : w = 0
     · simp [hw]
-    · by_cases hi₂ : i.val = 0
+    · by_cases hi₂ : i = 0
       · simp [hi₂]
-      · simp [Nat.lt_one_iff, hi₂, show 1 + (i.val - 1) = i by omega]
+      · simp [Nat.lt_one_iff, hi₂, h, show 1 + (i - 1) = i by omega]
 
 @[simp]
 theorem msb_shiftLeft {x : BitVec w} {n : Nat} :
@@ -1978,13 +2017,12 @@ theorem getElem_cons {b : Bool} {n} {x : BitVec n} {i : Nat} (h : i < n + 1) :
 
 theorem setWidth_succ (x : BitVec w) :
     setWidth (i+1) x = cons (getLsbD x i) (setWidth i x) := by
-  apply eq_of_getLsbD_eq
-  intro j
-  simp only [getLsbD_setWidth, getLsbD_cons, j.isLt, decide_true, Bool.true_and]
-  if j_eq : j.val = i then
+  ext j h
+  simp only [getLsbD_setWidth, getLsbD_cons, h, decide_true, Bool.true_and]
+  if j_eq : j = i then
     simp [j_eq]
   else
-    have j_lt : j.val < i := Nat.lt_of_le_of_ne (Nat.le_of_succ_le_succ j.isLt) j_eq
+    have j_lt : j < i := Nat.lt_of_le_of_ne (Nat.le_of_succ_le_succ h) j_eq
     simp [j_eq, j_lt]
 
 @[simp] theorem cons_msb_setWidth (x : BitVec (w+1)) : (cons x.msb (x.setWidth w)) = x := by
@@ -2098,19 +2136,19 @@ theorem msb_concat {w : Nat} {b : Bool} {x : BitVec w} :
   simp [← Fin.val_inj]
 
 @[simp] theorem not_concat (x : BitVec w) (b : Bool) : ~~~(concat x b) = concat (~~~x) !b := by
-  ext i; cases i using Fin.succRecOn <;> simp [*, Nat.succ_lt_succ]
+  ext (_ | i) h <;> simp [getLsbD_concat]
 
 @[simp] theorem concat_or_concat (x y : BitVec w) (a b : Bool) :
     (concat x a) ||| (concat y b) = concat (x ||| y) (a || b) := by
-  ext i; cases i using Fin.succRecOn <;> simp
+  ext (_ | i) h <;> simp [getLsbD_concat]
 
 @[simp] theorem concat_and_concat (x y : BitVec w) (a b : Bool) :
     (concat x a) &&& (concat y b) = concat (x &&& y) (a && b) := by
-  ext i; cases i using Fin.succRecOn <;> simp
+  ext (_ | i) h <;> simp [getLsbD_concat]
 
 @[simp] theorem concat_xor_concat (x y : BitVec w) (a b : Bool) :
     (concat x a) ^^^ (concat y b) = concat (x ^^^ y) (a ^^ b) := by
-  ext i; cases i using Fin.succRecOn <;> simp
+  ext (_ | i) h <;> simp [getLsbD_concat]
 
 @[simp] theorem zero_concat_false : concat 0#w false = 0#(w + 1) := by
   ext
@@ -2131,8 +2169,8 @@ theorem getLsbD_shiftConcat_eq_decide (x : BitVec w) (b : Bool) (i : Nat) :
 
 theorem shiftRight_sub_one_eq_shiftConcat (n : BitVec w) (hwn : 0 < wn) :
     n >>> (wn - 1) = (n >>> wn).shiftConcat (n.getLsbD (wn - 1)) := by
-  ext i
-  simp only [getLsbD_ushiftRight, getLsbD_shiftConcat, Fin.is_lt, decide_true, Bool.true_and]
+  ext i h
+  simp only [getLsbD_ushiftRight, getLsbD_shiftConcat, h, decide_true, Bool.true_and]
   split
   · simp [*]
   · congr 1; omega
@@ -3143,8 +3181,8 @@ theorem setWidth_setWidth_succ_eq_setWidth_setWidth_of_getLsbD_false
   {x : BitVec w} {i : Nat} (hx : x.getLsbD i = false) :
     setWidth w (x.setWidth (i + 1)) =
       setWidth w (x.setWidth i) := by
-  ext k
-  simp only [getLsbD_setWidth, Fin.is_lt, decide_true, Bool.true_and, getLsbD_or, getLsbD_and]
+  ext k h
+  simp only [getLsbD_setWidth, h, decide_true, Bool.true_and, getLsbD_or, getLsbD_and]
   by_cases hik : i = k
   · subst hik
     simp [hx]
@@ -3159,20 +3197,17 @@ theorem setWidth_setWidth_succ_eq_setWidth_setWidth_or_twoPow_of_getLsbD_true
     {x : BitVec w} {i : Nat} (hx : x.getLsbD i = true) :
     setWidth w (x.setWidth (i + 1)) =
       setWidth w (x.setWidth i) ||| (twoPow w i) := by
-  ext k
-  simp only [getLsbD_setWidth, Fin.is_lt, decide_true, Bool.true_and, getLsbD_or, getLsbD_and]
+  ext k h
+  simp only [getLsbD_setWidth, h, decide_true, Bool.true_and, getLsbD_or, getLsbD_and]
   by_cases hik : i = k
   · subst hik
-    simp [hx]
+    simp [hx, h]
   · by_cases hik' : k < i + 1 <;> simp [hik, hik'] <;> omega
 
 /-- Bitwise and of `(x : BitVec w)` with `1#w` equals zero extending `x.lsb` to `w`. -/
 theorem and_one_eq_setWidth_ofBool_getLsbD {x : BitVec w} :
     (x &&& 1#w) = setWidth w (ofBool (x.getLsbD 0)) := by
-  ext i
-  simp only [getLsbD_and, getLsbD_one, getLsbD_setWidth, Fin.is_lt, decide_true, getLsbD_ofBool,
-    Bool.true_and]
-  by_cases h : ((i : Nat) = 0) <;> simp [h] <;> omega
+  ext (_ | i) h <;> simp [Bool.and_comm]
 
 @[simp]
 theorem replicate_zero_eq {x : BitVec w} : x.replicate 0 = 0#0 := by
@@ -3196,7 +3231,7 @@ theorem getLsbD_replicate {n w : Nat} (x : BitVec w) :
     · simp only [hi, decide_true, Bool.true_and]
       by_cases hi' : i < w * n
       · simp [hi', ih]
-      · simp only [hi', decide_false, cond_false]
+      · simp [hi', decide_false]
         rw [Nat.sub_mul_eq_mod_of_lt_of_le] <;> omega
     · rw [Nat.mul_succ] at hi ⊢
       simp only [show ¬i < w * n by omega, decide_false, cond_false, hi, Bool.false_and]
@@ -3502,7 +3537,7 @@ theorem forall_zero_iff {P : BitVec 0 → Prop} :
   · intro h
     apply h
   · intro h v
-    obtain (rfl : v = 0#0) := (by ext ⟨i, h⟩; simp at h)
+    obtain (rfl : v = 0#0) := (by ext i ⟨⟩)
     apply h
 
 theorem forall_cons_iff {P : BitVec (n + 1) → Prop} :
@@ -3518,7 +3553,7 @@ theorem forall_cons_iff {P : BitVec (n + 1) → Prop} :
 instance instDecidableForallBitVecZero (P : BitVec 0 → Prop) :
     ∀ [Decidable (P 0#0)], Decidable (∀ v, P v)
   | .isTrue h => .isTrue fun v => by
-    obtain (rfl : v = 0#0) := (by ext ⟨i, h⟩; cases h)
+    obtain (rfl : v = 0#0) := (by ext i ⟨⟩)
     exact h
   | .isFalse h => .isFalse (fun w => h (w _))
 
@@ -3563,6 +3598,9 @@ instance instDecidableExistsBitVec :
 
 set_option linter.missingDocs false
 
+@[deprecated signExtend_eq_setWidth_of_msb_false (since := "2024-12-08")]
+abbrev signExtend_eq_not_setWidth_not_of_msb_false := @signExtend_eq_setWidth_of_msb_false
+
 @[deprecated truncate_eq_setWidth (since := "2024-09-18")]
 abbrev truncate_eq_zeroExtend := @truncate_eq_setWidth
 
@@ -3665,8 +3703,8 @@ abbrev truncate_xor := @setWidth_xor
 @[deprecated setWidth_not (since := "2024-09-18")]
 abbrev truncate_not := @setWidth_not
 
-@[deprecated signExtend_eq_not_setWidth_not_of_msb_false  (since := "2024-09-18")]
-abbrev signExtend_eq_not_zeroExtend_not_of_msb_false  := @signExtend_eq_not_setWidth_not_of_msb_false
+@[deprecated signExtend_eq_setWidth_of_msb_false  (since := "2024-09-18")]
+abbrev signExtend_eq_not_zeroExtend_not_of_msb_false  := @signExtend_eq_setWidth_of_msb_false
 
 @[deprecated signExtend_eq_not_setWidth_not_of_msb_true (since := "2024-09-18")]
 abbrev signExtend_eq_not_zeroExtend_not_of_msb_true := @signExtend_eq_not_setWidth_not_of_msb_true

src/Init/Data/Float32.lean

@@ -0,0 +1,180 @@
+/-
+Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Init.Core
+import Init.Data.Int.Basic
+import Init.Data.ToString.Basic
+import Init.Data.Float
+
+/-
+#exit -- TODO: Remove after update stage0
+
+-- Just show FloatSpec is inhabited.
+opaque float32Spec : FloatSpec := {
+  float := Unit,
+  val   := (),
+  lt    := fun _ _ => True,
+  le    := fun _ _ => True,
+  decLt := fun _ _ => inferInstanceAs (Decidable True),
+  decLe := fun _ _ => inferInstanceAs (Decidable True)
+}
+
+/-- Native floating point type, corresponding to the IEEE 754 *binary32* format
+(`float` in C or `f32` in Rust). -/
+structure Float32 where
+  val : float32Spec.float
+
+instance : Nonempty Float32 := ⟨{ val := float32Spec.val }⟩
+
+@[extern "lean_float32_add"] opaque Float32.add : Float32 → Float32 → Float32
+@[extern "lean_float32_sub"] opaque Float32.sub : Float32 → Float32 → Float32
+@[extern "lean_float32_mul"] opaque Float32.mul : Float32 → Float32 → Float32
+@[extern "lean_float32_div"] opaque Float32.div : Float32 → Float32 → Float32
+@[extern "lean_float32_negate"] opaque Float32.neg : Float32 → Float32
+
+set_option bootstrap.genMatcherCode false
+def Float32.lt : Float32 → Float32 → Prop := fun a b =>
+  match a, b with
+  | ⟨a⟩, ⟨b⟩ => float32Spec.lt a b
+
+def Float32.le : Float32 → Float32 → Prop := fun a b =>
+  float32Spec.le a.val b.val
+
+/--
+Raw transmutation from `UInt32`.
+
+Float32s and UInts have the same endianness on all supported platforms.
+IEEE 754 very precisely specifies the bit layout of floats.
+-/
+@[extern "lean_float32_of_bits"] opaque Float32.ofBits : UInt32 → Float32
+
+/--
+Raw transmutation to `UInt32`.
+
+Float32s and UInts have the same endianness on all supported platforms.
+IEEE 754 very precisely specifies the bit layout of floats.
+
+Note that this function is distinct from `Float32.toUInt32`, which attempts
+to preserve the numeric value, and not the bitwise value.
+-/
+@[extern "lean_float32_to_bits"] opaque Float32.toBits : Float32 → UInt32
+
+instance : Add Float32 := ⟨Float32.add⟩
+instance : Sub Float32 := ⟨Float32.sub⟩
+instance : Mul Float32 := ⟨Float32.mul⟩
+instance : Div Float32 := ⟨Float32.div⟩
+instance : Neg Float32 := ⟨Float32.neg⟩
+instance : LT Float32  := ⟨Float32.lt⟩
+instance : LE Float32  := ⟨Float32.le⟩
+
+/-- Note: this is not reflexive since `NaN != NaN`.-/
+@[extern "lean_float32_beq"] opaque Float32.beq (a b : Float32) : Bool
+
+instance : BEq Float32 := ⟨Float32.beq⟩
+
+@[extern "lean_float32_decLt"] opaque Float32.decLt (a b : Float32) : Decidable (a < b) :=
+  match a, b with
+  | ⟨a⟩, ⟨b⟩ => float32Spec.decLt a b
+
+@[extern "lean_float32_decLe"] opaque Float32.decLe (a b : Float32) : Decidable (a ≤ b) :=
+  match a, b with
+  | ⟨a⟩, ⟨b⟩ => float32Spec.decLe a b
+
+instance float32DecLt (a b : Float32) : Decidable (a < b) := Float32.decLt a b
+instance float32DecLe (a b : Float32) : Decidable (a ≤ b) := Float32.decLe a b
+
+@[extern "lean_float32_to_string"] opaque Float32.toString : Float32 → String
+/-- If the given float is non-negative, truncates the value to the nearest non-negative integer.
+If negative or NaN, returns `0`.
+If larger than the maximum value for `UInt8` (including Inf), returns the maximum value of `UInt8`
+(i.e. `UInt8.size - 1`).
+-/
+@[extern "lean_float32_to_uint8"] opaque Float32.toUInt8 : Float32 → UInt8
+/-- If the given float is non-negative, truncates the value to the nearest non-negative integer.
+If negative or NaN, returns `0`.
+If larger than the maximum value for `UInt16` (including Inf), returns the maximum value of `UInt16`
+(i.e. `UInt16.size - 1`).
+-/
+@[extern "lean_float32_to_uint16"] opaque Float32.toUInt16 : Float32 → UInt16
+/-- If the given float is non-negative, truncates the value to the nearest non-negative integer.
+If negative or NaN, returns `0`.
+If larger than the maximum value for `UInt32` (including Inf), returns the maximum value of `UInt32`
+(i.e. `UInt32.size - 1`).
+-/
+@[extern "lean_float32_to_uint32"] opaque Float32.toUInt32 : Float32 → UInt32
+/-- If the given float is non-negative, truncates the value to the nearest non-negative integer.
+If negative or NaN, returns `0`.
+If larger than the maximum value for `UInt64` (including Inf), returns the maximum value of `UInt64`
+(i.e. `UInt64.size - 1`).
+-/
+@[extern "lean_float32_to_uint64"] opaque Float32.toUInt64 : Float32 → UInt64
+/-- If the given float is non-negative, truncates the value to the nearest non-negative integer.
+If negative or NaN, returns `0`.
+If larger than the maximum value for `USize` (including Inf), returns the maximum value of `USize`
+(i.e. `USize.size - 1`). This value is platform dependent).
+-/
+@[extern "lean_float32_to_usize"] opaque Float32.toUSize : Float32 → USize
+
+@[extern "lean_float32_isnan"] opaque Float32.isNaN : Float32 → Bool
+@[extern "lean_float32_isfinite"] opaque Float32.isFinite : Float32 → Bool
+@[extern "lean_float32_isinf"] opaque Float32.isInf : Float32 → Bool
+/-- Splits the given float `x` into a significand/exponent pair `(s, i)`
+such that `x = s * 2^i` where `s ∈ (-1;-0.5] ∪ [0.5; 1)`.
+Returns an undefined value if `x` is not finite.
+-/
+@[extern "lean_float32_frexp"] opaque Float32.frExp : Float32 → Float32 × Int
+
+instance : ToString Float32 where
+  toString := Float32.toString
+
+@[extern "lean_uint64_to_float"] opaque UInt64.toFloat32 (n : UInt64) : Float32
+
+instance : Inhabited Float32 where
+  default := UInt64.toFloat32 0
+
+instance : Repr Float32 where
+  reprPrec n prec := if n < UInt64.toFloat32 0 then Repr.addAppParen (toString n) prec else toString n
+
+instance : ReprAtom Float32  := ⟨⟩
+
+@[extern "sinf"] opaque Float32.sin : Float32 → Float32
+@[extern "cosf"] opaque Float32.cos : Float32 → Float32
+@[extern "tanf"] opaque Float32.tan : Float32 → Float32
+@[extern "asinf"] opaque Float32.asin : Float32 → Float32
+@[extern "acosf"] opaque Float32.acos : Float32 → Float32
+@[extern "atanf"] opaque Float32.atan : Float32 → Float32
+@[extern "atan2f"] opaque Float32.atan2 : Float32 → Float32 → Float32
+@[extern "sinhf"] opaque Float32.sinh : Float32 → Float32
+@[extern "coshf"] opaque Float32.cosh : Float32 → Float32
+@[extern "tanhf"] opaque Float32.tanh : Float32 → Float32
+@[extern "asinhf"] opaque Float32.asinh : Float32 → Float32
+@[extern "acoshf"] opaque Float32.acosh : Float32 → Float32
+@[extern "atanhf"] opaque Float32.atanh : Float32 → Float32
+@[extern "expf"] opaque Float32.exp : Float32 → Float32
+@[extern "exp2f"] opaque Float32.exp2 : Float32 → Float32
+@[extern "logf"] opaque Float32.log : Float32 → Float32
+@[extern "log2f"] opaque Float32.log2 : Float32 → Float32
+@[extern "log10f"] opaque Float32.log10 : Float32 → Float32
+@[extern "powf"] opaque Float32.pow : Float32 → Float32 → Float32
+@[extern "sqrtf"] opaque Float32.sqrt : Float32 → Float32
+@[extern "cbrtf"] opaque Float32.cbrt : Float32 → Float32
+@[extern "ceilf"] opaque Float32.ceil : Float32 → Float32
+@[extern "floorf"] opaque Float32.floor : Float32 → Float32
+@[extern "roundf"] opaque Float32.round : Float32 → Float32
+@[extern "fabsf"] opaque Float32.abs : Float32 → Float32
+
+instance : HomogeneousPow Float32 := ⟨Float32.pow⟩
+
+instance : Min Float32 := minOfLe
+
+instance : Max Float32 := maxOfLe
+
+/--
+Efficiently computes `x * 2^i`.
+-/
+@[extern "lean_float32_scaleb"]
+opaque Float32.scaleB (x : Float32) (i : @& Int) : Float32
+-/

src/Init/Data/List.lean

@@ -24,6 +24,7 @@ import Init.Data.List.Zip
 import Init.Data.List.Perm
 import Init.Data.List.Sort
 import Init.Data.List.ToArray
+import Init.Data.List.ToArrayImpl
 import Init.Data.List.MapIdx
 import Init.Data.List.OfFn
 import Init.Data.List.FinRange

src/Init/Data/List/Basic.lean

@@ -666,10 +666,14 @@ def isEmpty : List α → Bool
 /-! ### elem -/
 
 /--
-`O(|l|)`. `elem a l` or `l.contains a` is true if there is an element in `l` equal to `a`.
+`O(|l|)`.
+`l.contains a` or `elem a l` is true if there is an element in `l` equal (according to `==`) to `a`.
 
-* `elem 3 [1, 4, 2, 3, 3, 7] = true`
-* `elem 5 [1, 4, 2, 3, 3, 7] = false`
+* `[1, 4, 2, 3, 3, 7].contains 3 = true`
+* `[1, 4, 2, 3, 3, 7].contains 5 = false`
+
+The preferred simp normal form is `l.contains a`, and when `LawfulBEq α` is available,
+`l.contains a = true ↔ a ∈ l` and `l.contains a = false ↔ a ∉ l`.
 -/
 def elem [BEq α] (a : α) : List α → Bool
   | []    => false

src/Init/Data/List/Lemmas.lean

@@ -220,15 +220,6 @@ We simplify `l[n]!` to `(l[n]?).getD default`.
 
 /-! ### getElem? and getElem -/
 
-@[simp] theorem getElem?_eq_getElem {l : List α} {n} (h : n < l.length) : l[n]? = some l[n] := by
-  simp only [getElem?_def, h, ↓reduceDIte]
-
-theorem getElem?_eq_some_iff {l : List α} : l[n]? = some a ↔ ∃ h : n < l.length, l[n] = a := by
-  simp only [← get?_eq_getElem?, get?_eq_some_iff, get_eq_getElem]
-
-theorem some_eq_getElem?_iff {l : List α} : some a = l[n]? ↔ ∃ h : n < l.length, l[n] = a := by
-  rw [eq_comm, getElem?_eq_some_iff]
-
 @[simp] theorem getElem?_eq_none_iff : l[n]? = none ↔ length l ≤ n := by
   simp only [← get?_eq_getElem?, get?_eq_none_iff]
 
@@ -237,11 +228,20 @@ theorem some_eq_getElem?_iff {l : List α} : some a = l[n]? ↔ ∃ h : n < l.le
 
 theorem getElem?_eq_none (h : length l ≤ n) : l[n]? = none := getElem?_eq_none_iff.mpr h
 
-@[simp] theorem some_getElem_eq_getElem?_iff {α} (xs : List α) (i : Nat) (h : i < xs.length) :
+@[simp] theorem getElem?_eq_getElem {l : List α} {n} (h : n < l.length) : l[n]? = some l[n] :=
+  getElem?_pos ..
+
+theorem getElem?_eq_some_iff {l : List α} : l[n]? = some a ↔ ∃ h : n < l.length, l[n] = a := by
+  simp only [← get?_eq_getElem?, get?_eq_some_iff, get_eq_getElem]
+
+theorem some_eq_getElem?_iff {l : List α} : some a = l[n]? ↔ ∃ h : n < l.length, l[n] = a := by
+  rw [eq_comm, getElem?_eq_some_iff]
+
+@[simp] theorem some_getElem_eq_getElem?_iff (xs : List α) (i : Nat) (h : i < xs.length) :
     (some xs[i] = xs[i]?) ↔ True := by
   simp [h]
 
-@[simp] theorem getElem?_eq_some_getElem_iff {α} (xs : List α) (i : Nat) (h : i < xs.length) :
+@[simp] theorem getElem?_eq_some_getElem_iff (xs : List α) (i : Nat) (h : i < xs.length) :
     (xs[i]? = some xs[i]) ↔ True := by
   simp [h]
 
@@ -253,8 +253,21 @@ theorem getElem_eq_getElem?_get (l : List α) (i : Nat) (h : i < l.length) :
     l[i] = l[i]?.get (by simp [getElem?_eq_getElem, h]) := by
   simp [getElem_eq_iff]
 
+theorem getD_getElem? (l : List α) (i : Nat) (d : α) :
+    l[i]?.getD d = if p : i < l.length then l[i]'p else d := by
+  if h : i < l.length then
+    simp [h, getElem?_def]
+  else
+    have p : i ≥ l.length := Nat.le_of_not_gt h
+    simp [getElem?_eq_none p, h]
+
 @[simp] theorem getElem?_nil {n : Nat} : ([] : List α)[n]? = none := rfl
 
+theorem getElem_cons {l : List α} (w : i < (a :: l).length) :
+    (a :: l)[i] =
+      if h : i = 0 then a else l[i-1]'(match i, h with | i+1, _ => succ_lt_succ_iff.mp w) := by
+  cases i <;> simp
+
 theorem getElem?_cons_zero {l : List α} : (a::l)[0]? = some a := by simp
 
 @[simp] theorem getElem?_cons_succ {l : List α} : (a::l)[n+1]? = l[n]? := by
@@ -264,6 +277,13 @@ theorem getElem?_cons_zero {l : List α} : (a::l)[0]? = some a := by simp
 theorem getElem?_cons : (a :: l)[i]? = if i = 0 then some a else l[i-1]? := by
   cases i <;> simp
 
+@[simp] theorem getElem_singleton (a : α) (h : i < 1) : [a][i] = a :=
+  match i, h with
+  | 0, _ => rfl
+
+theorem getElem?_singleton (a : α) (i : Nat) : [a][i]? = if i = 0 then some a else none := by
+  simp [getElem?_cons]
+
 /--
 If one has `l[i]` in an expression and `h : l = l'`,
 `rw [h]` will give a "motive it not type correct" error, as it cannot rewrite the
@@ -273,10 +293,6 @@ such a rewrite, with `rw [getElem_of_eq h]`.
 theorem getElem_of_eq {l l' : List α} (h : l = l') {i : Nat} (w : i < l.length) :
     l[i] = l'[i]'(h ▸ w) := by cases h; rfl
 
-@[simp] theorem getElem_singleton (a : α) (h : i < 1) : [a][i] = a :=
-  match i, h with
-  | 0, _ => rfl
-
 theorem getElem_zero {l : List α} (h : 0 < l.length) : l[0] = l.head (length_pos.mp h) :=
   match l, h with
   | _ :: _, _ => rfl
@@ -300,12 +316,6 @@ theorem ext_getElem {l₁ l₂ : List α} (hl : length l₁ = length l₂)
 theorem getElem?_concat_length (l : List α) (a : α) : (l ++ [a])[l.length]? = some a := by
   simp
 
-theorem isSome_getElem? {l : List α} {n : Nat} : l[n]?.isSome ↔ n < l.length := by
-  simp
-
-theorem isNone_getElem? {l : List α} {n : Nat} : l[n]?.isNone ↔ l.length ≤ n := by
-  simp
-
 /-! ### mem -/
 
 @[simp] theorem not_mem_nil (a : α) : ¬ a ∈ [] := nofun
@@ -449,6 +459,10 @@ theorem forall_getElem {l : List α} {p : α → Prop} :
         simp only [getElem_cons_succ]
         exact getElem_mem (lt_of_succ_lt_succ h)
 
+@[simp] theorem elem_eq_contains [BEq α] {a : α} {l : List α} :
+    elem a l = l.contains a := by
+  simp [contains]
+
 @[simp] theorem decide_mem_cons [BEq α] [LawfulBEq α] {l : List α} :
     decide (y ∈ a :: l) = (y == a || decide (y ∈ l)) := by
   cases h : y == a <;> simp_all
@@ -456,16 +470,27 @@ theorem forall_getElem {l : List α} {p : α → Prop} :
 theorem elem_iff [BEq α] [LawfulBEq α] {a : α} {as : List α} :
     elem a as = true ↔ a ∈ as := ⟨mem_of_elem_eq_true, elem_eq_true_of_mem⟩
 
-@[simp] theorem elem_eq_mem [BEq α] [LawfulBEq α] (a : α) (as : List α) :
+theorem contains_iff [BEq α] [LawfulBEq α] {a : α} {as : List α} :
+    as.contains a = true ↔ a ∈ as := ⟨mem_of_elem_eq_true, elem_eq_true_of_mem⟩
+
+theorem elem_eq_mem [BEq α] [LawfulBEq α] (a : α) (as : List α) :
     elem a as = decide (a ∈ as) := by rw [Bool.eq_iff_iff, elem_iff, decide_eq_true_iff]
 
+@[simp] theorem contains_eq_mem [BEq α] [LawfulBEq α] (a : α) (as : List α) :
+    as.contains a = decide (a ∈ as) := by rw [Bool.eq_iff_iff, elem_iff, decide_eq_true_iff]
+
+@[simp] theorem contains_cons [BEq α] {a : α} {b : α} {l : List α} :
+    (a :: l).contains b = (b == a || l.contains b) := by
+  simp only [contains, elem_cons]
+  split <;> simp_all
+
 /-! ### `isEmpty` -/
 
 theorem isEmpty_iff {l : List α} : l.isEmpty ↔ l = [] := by
   cases l <;> simp
 
 theorem isEmpty_eq_false_iff_exists_mem {xs : List α} :
-    (List.isEmpty xs = false) ↔ ∃ x, x ∈ xs := by
+    xs.isEmpty = false ↔ ∃ x, x ∈ xs := by
   cases xs <;> simp
 
 theorem isEmpty_iff_length_eq_zero {l : List α} : l.isEmpty ↔ l.length = 0 := by
@@ -503,17 +528,21 @@ theorem decide_forall_mem {l : List α} {p : α → Prop} [DecidablePred p] :
 @[simp] theorem all_eq_false {l : List α} : l.all p = false ↔ ∃ x, x ∈ l ∧ ¬p x := by
   simp [all_eq]
 
-theorem any_beq [BEq α] [LawfulBEq α] {l : List α} : (l.any fun x => a == x) ↔ a ∈ l := by
-  simp
+theorem any_beq [BEq α] {l : List α} {a : α} : (l.any fun x => a == x) = l.contains a := by
+  induction l <;> simp_all [contains_cons]
 
-theorem any_beq' [BEq α] [LawfulBEq α] {l : List α} : (l.any fun x => x == a) ↔ a ∈ l := by
-  simp
+/-- Variant of `any_beq` with `==` reversed. -/
+theorem any_beq' [BEq α] [PartialEquivBEq α] {l : List α} :
+    (l.any fun x => x == a) = l.contains a := by
+  simp only [BEq.comm, any_beq]
 
-theorem all_bne [BEq α] [LawfulBEq α] {l : List α} : (l.all fun x => a != x) ↔ a ∉ l := by
-  induction l <;> simp_all
+theorem all_bne [BEq α] {l : List α} : (l.all fun x => a != x) = !l.contains a := by
+  induction l <;> simp_all [bne]
 
-theorem all_bne' [BEq α] [LawfulBEq α] {l : List α} : (l.all fun x => x != a) ↔ a ∉ l := by
-  induction l <;> simp_all [eq_comm (a := a)]
+/-- Variant of `all_bne` with `!=` reversed. -/
+theorem all_bne' [BEq α] [PartialEquivBEq α] {l : List α} :
+    (l.all fun x => x != a) = !l.contains a := by
+  simp only [bne_comm, all_bne]
 
 /-! ### set -/
 
@@ -2826,11 +2855,6 @@ theorem leftpad_suffix (n : Nat) (a : α) (l : List α) : l <:+ (leftpad n a l)
 
 theorem elem_cons_self [BEq α] [LawfulBEq α] {a : α} : (a::as).elem a = true := by simp
 
-@[simp] theorem contains_cons [BEq α] :
-    (a :: as : List α).contains x = (x == a || as.contains x) := by
-  simp only [contains, elem]
-  split <;> simp_all
-
 theorem contains_eq_any_beq [BEq α] (l : List α) (a : α) : l.contains a = l.any (a == ·) := by
   induction l with simp | cons b l => cases b == a <;> simp [*]
 
@@ -3529,7 +3553,12 @@ theorem getElem?_eq (l : List α) (i : Nat) :
   getElem?_def _ _
 @[deprecated getElem?_eq_none (since := "2024-11-29")] abbrev getElem?_len_le := @getElem?_eq_none
 
+@[deprecated _root_.isSome_getElem? (since := "2024-12-09")]
+theorem isSome_getElem? {l : List α} {n : Nat} : l[n]?.isSome ↔ n < l.length := by
+  simp
 
-
+@[deprecated _root_.isNone_getElem? (since := "2024-12-09")]
+theorem isNone_getElem? {l : List α} {n : Nat} : l[n]?.isNone ↔ l.length ≤ n := by
+  simp
 
 end List

src/Init/Data/List/MapIdx.lean

@@ -237,15 +237,15 @@ theorem getElem?_mapIdx_go : ∀ {l : List α} {arr : Array β} {i : Nat},
       if h : i < arr.size then some arr[i] else Option.map (f i) l[i - arr.size]?
   | [], arr, i => by
     simp only [mapIdx.go, Array.toListImpl_eq, getElem?_def, Array.length_toList,
-      Array.getElem_eq_getElem_toList, length_nil, Nat.not_lt_zero, ↓reduceDIte, Option.map_none']
+      ← Array.getElem_toList, length_nil, Nat.not_lt_zero, ↓reduceDIte, Option.map_none']
   | a :: l, arr, i => by
     rw [mapIdx.go, getElem?_mapIdx_go]
     simp only [Array.size_push]
     split <;> split
     · simp only [Option.some.injEq]
-      rw [Array.getElem_eq_getElem_toList]
+      rw [← Array.getElem_toList]
       simp only [Array.push_toList]
-      rw [getElem_append_left, Array.getElem_eq_getElem_toList]
+      rw [getElem_append_left, ← Array.getElem_toList]
     · have : i = arr.size := by omega
       simp_all
     · omega

src/Init/Data/List/ToArray.lean

@@ -1,23 +1,374 @@
 /-
-Copyright (c) 2024 Lean FRO. All rights reserved.
+Copyright (c) 2022 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Henrik Böving
+Authors: Mario Carneiro
 -/
 prelude
-import Init.Data.List.Basic
+import Init.Data.List.Impl
+import Init.Data.List.Nat.Erase
+import Init.Data.List.Monadic
 
-/--
-Auxiliary definition for `List.toArray`.
-`List.toArrayAux as r = r ++ as.toArray`
+/-! ### Lemmas about `List.toArray`.
+
+We prefer to pull `List.toArray` outwards past `Array` operations.
 -/
-@[inline_if_reduce]
-def List.toArrayAux : List α → Array α → Array α
-  | nil,       r => r
-  | cons a as, r => toArrayAux as (r.push a)
+namespace List
 
-/-- Convert a `List α` into an `Array α`. This is O(n) in the length of the list.  -/
--- This function is exported to C, where it is called by `Array.mk`
--- (the constructor) to implement this functionality.
-@[inline, match_pattern, pp_nodot, export lean_list_to_array]
-def List.toArrayImpl (as : List α) : Array α :=
-  as.toArrayAux (Array.mkEmpty as.length)
+open Array
+
+theorem toArray_inj {a b : List α} (h : a.toArray = b.toArray) : a = b := by
+  cases a with
+  | nil => simpa using h
+  | cons a as =>
+    cases b with
+    | nil => simp at h
+    | cons b bs => simpa using h
+
+@[simp] theorem size_toArrayAux {a : List α} {b : Array α} :
+    (a.toArrayAux b).size = b.size + a.length := by
+  simp [size]
+
+@[simp] theorem push_toArray (l : List α) (a : α) : l.toArray.push a = (l ++ [a]).toArray := by
+  apply ext'
+  simp
+
+/-- Unapplied variant of `push_toArray`, useful for monadic reasoning. -/
+@[simp] theorem push_toArray_fun (l : List α) : l.toArray.push = fun a => (l ++ [a]).toArray := by
+  funext a
+  simp
+
+@[simp] theorem isEmpty_toArray (l : List α) : l.toArray.isEmpty = l.isEmpty := by
+  cases l <;> simp
+
+@[simp] theorem toArray_singleton (a : α) : (List.singleton a).toArray = singleton a := rfl
+
+@[simp] theorem back!_toArray [Inhabited α] (l : List α) : l.toArray.back! = l.getLast! := by
+  simp only [back!, size_toArray, Array.get!_eq_getElem!, getElem!_toArray, getLast!_eq_getElem!]
+
+@[simp] theorem back?_toArray (l : List α) : l.toArray.back? = l.getLast? := by
+  simp [back?, List.getLast?_eq_getElem?]
+
+@[simp] theorem set_toArray (l : List α) (i : Nat) (a : α) (h : i < l.length) :
+    (l.toArray.set i a) = (l.set i a).toArray := rfl
+
+@[simp] theorem forIn'_loop_toArray [Monad m] (l : List α) (f : (a : α) → a ∈ l.toArray → β → m (ForInStep β)) (i : Nat)
+    (h : i ≤ l.length) (b : β) :
+    Array.forIn'.loop l.toArray f i h b =
+      forIn' (l.drop (l.length - i)) b (fun a m b => f a (by simpa using mem_of_mem_drop m) b) := by
+  induction i generalizing l b with
+  | zero =>
+    simp [Array.forIn'.loop]
+  | succ i ih =>
+    simp only [Array.forIn'.loop, size_toArray, getElem_toArray, ih]
+    have t : drop (l.length - (i + 1)) l = l[l.length - i - 1] :: drop (l.length - i) l := by
+      simp only [Nat.sub_add_eq]
+      rw [List.drop_sub_one (by omega), List.getElem?_eq_getElem (by omega)]
+      simp only [Option.toList_some, singleton_append]
+    simp [t]
+    have t : l.length - 1 - i = l.length - i - 1 := by omega
+    simp only [t]
+    congr
+
+@[simp] theorem forIn'_toArray [Monad m] (l : List α) (b : β) (f : (a : α) → a ∈ l.toArray → β → m (ForInStep β)) :
+    forIn' l.toArray b f = forIn' l b (fun a m b => f a (mem_toArray.mpr m) b) := by
+  change Array.forIn' _ _ _ = List.forIn' _ _ _
+  rw [Array.forIn', forIn'_loop_toArray]
+  simp
+
+@[simp] theorem forIn_toArray [Monad m] (l : List α) (b : β) (f : α → β → m (ForInStep β)) :
+    forIn l.toArray b f = forIn l b f := by
+  simpa using forIn'_toArray l b fun a m b => f a b
+
+theorem foldrM_toArray [Monad m] (f : α → β → m β) (init : β) (l : List α) :
+    l.toArray.foldrM f init = l.foldrM f init := by
+  rw [foldrM_eq_reverse_foldlM_toList]
+  simp
+
+theorem foldlM_toArray [Monad m] (f : β → α → m β) (init : β) (l : List α) :
+    l.toArray.foldlM f init = l.foldlM f init := by
+  rw [foldlM_toList]
+
+theorem foldr_toArray (f : α → β → β) (init : β) (l : List α) :
+    l.toArray.foldr f init = l.foldr f init := by
+  rw [foldr_toList]
+
+theorem foldl_toArray (f : β → α → β) (init : β) (l : List α) :
+    l.toArray.foldl f init = l.foldl f init := by
+  rw [foldl_toList]
+
+/-- Variant of `foldrM_toArray` with a side condition for the `start` argument. -/
+@[simp] theorem foldrM_toArray' [Monad m] (f : α → β → m β) (init : β) (l : List α)
+    (h : start = l.toArray.size) :
+    l.toArray.foldrM f init start 0 = l.foldrM f init := by
+  subst h
+  rw [foldrM_eq_reverse_foldlM_toList]
+  simp
+
+/-- Variant of `foldlM_toArray` with a side condition for the `stop` argument. -/
+@[simp] theorem foldlM_toArray' [Monad m] (f : β → α → m β) (init : β) (l : List α)
+    (h : stop = l.toArray.size) :
+    l.toArray.foldlM f init 0 stop = l.foldlM f init := by
+  subst h
+  rw [foldlM_toList]
+
+/-- Variant of `foldr_toArray` with a side condition for the `start` argument. -/
+@[simp] theorem foldr_toArray' (f : α → β → β) (init : β) (l : List α)
+    (h : start = l.toArray.size) :
+    l.toArray.foldr f init start 0 = l.foldr f init := by
+  subst h
+  rw [foldr_toList]
+
+/-- Variant of `foldl_toArray` with a side condition for the `stop` argument. -/
+@[simp] theorem foldl_toArray' (f : β → α → β) (init : β) (l : List α)
+    (h : stop = l.toArray.size) :
+    l.toArray.foldl f init 0 stop = l.foldl f init := by
+  subst h
+  rw [foldl_toList]
+
+@[simp] theorem append_toArray (l₁ l₂ : List α) :
+    l₁.toArray ++ l₂.toArray = (l₁ ++ l₂).toArray := by
+  apply ext'
+  simp
+
+@[simp] theorem push_append_toArray {as : Array α} {a : α} {bs : List α} : as.push a ++ bs.toArray = as ++ (a ::bs).toArray := by
+  cases as
+  simp
+
+@[simp] theorem foldl_push {l : List α} {as : Array α} : l.foldl Array.push as = as ++ l.toArray := by
+  induction l generalizing as <;> simp [*]
+
+@[simp] theorem foldr_push {l : List α} {as : Array α} : l.foldr (fun a b => push b a) as = as ++ l.reverse.toArray := by
+  rw [foldr_eq_foldl_reverse, foldl_push]
+
+@[simp] theorem findSomeM?_toArray [Monad m] [LawfulMonad m] (f : α → m (Option β)) (l : List α) :
+    l.toArray.findSomeM? f = l.findSomeM? f := by
+  rw [Array.findSomeM?]
+  simp only [bind_pure_comp, map_pure, forIn_toArray]
+  induction l with
+  | nil => simp
+  | cons a l ih =>
+    simp only [forIn_cons, LawfulMonad.bind_assoc, findSomeM?]
+    congr
+    ext1 (_|_) <;> simp [ih]
+
+theorem findSomeRevM?_find_toArray [Monad m] [LawfulMonad m] (f : α → m (Option β)) (l : List α)
+    (i : Nat) (h) :
+    findSomeRevM?.find f l.toArray i h = (l.take i).reverse.findSomeM? f := by
+  induction i generalizing l with
+  | zero => simp [Array.findSomeRevM?.find.eq_def]
+  | succ i ih =>
+    rw [size_toArray] at h
+    rw [Array.findSomeRevM?.find, take_succ, getElem?_eq_getElem (by omega)]
+    simp only [ih, reverse_append]
+    congr
+    ext1 (_|_) <;> simp
+
+-- This is not marked as `@[simp]` as later we simplify all occurrences of `findSomeRevM?`.
+theorem findSomeRevM?_toArray [Monad m] [LawfulMonad m] (f : α → m (Option β)) (l : List α) :
+    l.toArray.findSomeRevM? f = l.reverse.findSomeM? f := by
+  simp [Array.findSomeRevM?, findSomeRevM?_find_toArray]
+
+-- This is not marked as `@[simp]` as later we simplify all occurrences of `findRevM?`.
+theorem findRevM?_toArray [Monad m] [LawfulMonad m] (f : α → m Bool) (l : List α) :
+    l.toArray.findRevM? f = l.reverse.findM? f := by
+  rw [Array.findRevM?, findSomeRevM?_toArray, findM?_eq_findSomeM?]
+
+@[simp] theorem findM?_toArray [Monad m] [LawfulMonad m] (f : α → m Bool) (l : List α) :
+    l.toArray.findM? f = l.findM? f := by
+  rw [Array.findM?]
+  simp only [bind_pure_comp, map_pure, forIn_toArray]
+  induction l with
+  | nil => simp
+  | cons a l ih =>
+    simp only [forIn_cons, LawfulMonad.bind_assoc, findM?]
+    congr
+    ext1 (_|_) <;> simp [ih]
+
+@[simp] theorem findSome?_toArray (f : α → Option β) (l : List α) :
+    l.toArray.findSome? f = l.findSome? f := by
+  rw [Array.findSome?, ← findSomeM?_id, findSomeM?_toArray, Id.run]
+
+@[simp] theorem find?_toArray (f : α → Bool) (l : List α) :
+    l.toArray.find? f = l.find? f := by
+  rw [Array.find?]
+  simp only [Id.run, Id, Id.pure_eq, Id.bind_eq, forIn_toArray]
+  induction l with
+  | nil => simp
+  | cons a l ih =>
+    simp only [forIn_cons, Id.pure_eq, Id.bind_eq, find?]
+    by_cases f a <;> simp_all
+
+theorem isPrefixOfAux_toArray_succ [BEq α] (l₁ l₂ : List α) (hle : l₁.length ≤ l₂.length) (i : Nat) :
+    Array.isPrefixOfAux l₁.toArray l₂.toArray hle (i + 1) =
+      Array.isPrefixOfAux l₁.tail.toArray l₂.tail.toArray (by simp; omega) i := by
+  rw [Array.isPrefixOfAux]
+  conv => rhs; rw [Array.isPrefixOfAux]
+  simp only [size_toArray, getElem_toArray, Bool.if_false_right, length_tail, getElem_tail]
+  split <;> rename_i h₁ <;> split <;> rename_i h₂
+  · rw [isPrefixOfAux_toArray_succ]
+  · omega
+  · omega
+  · rfl
+
+theorem isPrefixOfAux_toArray_succ' [BEq α] (l₁ l₂ : List α) (hle : l₁.length ≤ l₂.length) (i : Nat) :
+    Array.isPrefixOfAux l₁.toArray l₂.toArray hle (i + 1) =
+      Array.isPrefixOfAux (l₁.drop (i+1)).toArray (l₂.drop (i+1)).toArray (by simp; omega) 0 := by
+  induction i generalizing l₁ l₂ with
+  | zero => simp [isPrefixOfAux_toArray_succ]
+  | succ i ih =>
+    rw [isPrefixOfAux_toArray_succ, ih]
+    simp
+
+theorem isPrefixOfAux_toArray_zero [BEq α] (l₁ l₂ : List α) (hle : l₁.length ≤ l₂.length) :
+    Array.isPrefixOfAux l₁.toArray l₂.toArray hle 0 =
+      l₁.isPrefixOf l₂ := by
+  rw [Array.isPrefixOfAux]
+  match l₁, l₂ with
+  | [], _ => rw [dif_neg] <;> simp
+  | _::_, [] => simp at hle
+  | a::l₁, b::l₂ =>
+    simp [isPrefixOf_cons₂, isPrefixOfAux_toArray_succ', isPrefixOfAux_toArray_zero]
+
+@[simp] theorem isPrefixOf_toArray [BEq α] (l₁ l₂ : List α) :
+    l₁.toArray.isPrefixOf l₂.toArray = l₁.isPrefixOf l₂ := by
+  rw [Array.isPrefixOf]
+  split <;> rename_i h
+  · simp [isPrefixOfAux_toArray_zero]
+  · simp only [Bool.false_eq]
+    induction l₁ generalizing l₂ with
+    | nil => simp at h
+    | cons a l₁ ih =>
+      cases l₂ with
+      | nil => simp
+      | cons b l₂ =>
+        simp only [isPrefixOf_cons₂, Bool.and_eq_false_imp]
+        intro w
+        rw [ih]
+        simp_all
+
+theorem zipWithAux_toArray_succ (as : List α) (bs : List β) (f : α → β → γ) (i : Nat) (cs : Array γ) :
+    zipWithAux as.toArray bs.toArray f (i + 1) cs = zipWithAux as.tail.toArray bs.tail.toArray f i cs := by
+  rw [zipWithAux]
+  conv => rhs; rw [zipWithAux]
+  simp only [size_toArray, getElem_toArray, length_tail, getElem_tail]
+  split <;> rename_i h₁
+  · split <;> rename_i h₂
+    · rw [dif_pos (by omega), dif_pos (by omega), zipWithAux_toArray_succ]
+    · rw [dif_pos (by omega)]
+      rw [dif_neg (by omega)]
+  · rw [dif_neg (by omega)]
+
+theorem zipWithAux_toArray_succ' (as : List α) (bs : List β) (f : α → β → γ) (i : Nat) (cs : Array γ) :
+    zipWithAux as.toArray bs.toArray f (i + 1) cs = zipWithAux (as.drop (i+1)).toArray (bs.drop (i+1)).toArray f 0 cs := by
+  induction i generalizing as bs cs with
+  | zero => simp [zipWithAux_toArray_succ]
+  | succ i ih =>
+    rw [zipWithAux_toArray_succ, ih]
+    simp
+
+theorem zipWithAux_toArray_zero (f : α → β → γ) (as : List α) (bs : List β) (cs : Array γ) :
+    zipWithAux as.toArray bs.toArray f 0 cs = cs ++ (List.zipWith f as bs).toArray := by
+  rw [Array.zipWithAux]
+  match as, bs with
+  | [], _ => simp
+  | _, [] => simp
+  | a :: as, b :: bs =>
+    simp [zipWith_cons_cons, zipWithAux_toArray_succ', zipWithAux_toArray_zero, push_append_toArray]
+
+@[simp] theorem zipWith_toArray (as : List α) (bs : List β) (f : α → β → γ) :
+    Array.zipWith as.toArray bs.toArray f = (List.zipWith f as bs).toArray := by
+  rw [Array.zipWith]
+  simp [zipWithAux_toArray_zero]
+
+@[simp] theorem zip_toArray (as : List α) (bs : List β) :
+    Array.zip as.toArray bs.toArray = (List.zip as bs).toArray := by
+  simp [Array.zip, zipWith_toArray, zip]
+
+theorem zipWithAll_go_toArray (as : List α) (bs : List β) (f : Option α → Option β → γ) (i : Nat) (cs : Array γ) :
+    zipWithAll.go f as.toArray bs.toArray i cs = cs ++ (List.zipWithAll f (as.drop i) (bs.drop i)).toArray := by
+  unfold zipWithAll.go
+  split <;> rename_i h
+  · rw [zipWithAll_go_toArray]
+    simp at h
+    simp only [getElem?_toArray, push_append_toArray]
+    if ha : i < as.length then
+      if hb : i < bs.length then
+        rw [List.drop_eq_getElem_cons ha, List.drop_eq_getElem_cons hb]
+        simp only [ha, hb, getElem?_eq_getElem, zipWithAll_cons_cons]
+      else
+        simp only [Nat.not_lt] at hb
+        rw [List.drop_eq_getElem_cons ha]
+        rw [(drop_eq_nil_iff (l := bs)).mpr (by omega), (drop_eq_nil_iff (l := bs)).mpr (by omega)]
+        simp only [zipWithAll_nil, map_drop, map_cons]
+        rw [getElem?_eq_getElem ha]
+        rw [getElem?_eq_none hb]
+    else
+      if hb : i < bs.length then
+        simp only [Nat.not_lt] at ha
+        rw [List.drop_eq_getElem_cons hb]
+        rw [(drop_eq_nil_iff (l := as)).mpr (by omega), (drop_eq_nil_iff (l := as)).mpr (by omega)]
+        simp only [nil_zipWithAll, map_drop, map_cons]
+        rw [getElem?_eq_getElem hb]
+        rw [getElem?_eq_none ha]
+      else
+        omega
+  · simp only [size_toArray, Nat.not_lt] at h
+    rw [drop_eq_nil_of_le (by omega), drop_eq_nil_of_le (by omega)]
+    simp
+  termination_by max as.length bs.length - i
+  decreasing_by simp_wf; decreasing_trivial_pre_omega
+
+@[simp] theorem zipWithAll_toArray (f : Option α → Option β → γ) (as : List α) (bs : List β) :
+    Array.zipWithAll as.toArray bs.toArray f = (List.zipWithAll f as bs).toArray := by
+  simp [Array.zipWithAll, zipWithAll_go_toArray]
+
+@[simp] theorem toArray_appendList (l₁ l₂ : List α) :
+    l₁.toArray ++ l₂ = (l₁ ++ l₂).toArray := by
+  apply ext'
+  simp
+
+@[simp] theorem pop_toArray (l : List α) : l.toArray.pop = l.dropLast.toArray := by
+  apply ext'
+  simp
+
+theorem takeWhile_go_succ (p : α → Bool) (a : α) (l : List α) (i : Nat) :
+    takeWhile.go p (a :: l).toArray (i+1) r = takeWhile.go p l.toArray i r := by
+  rw [takeWhile.go, takeWhile.go]
+  simp only [size_toArray, length_cons, Nat.add_lt_add_iff_right, Array.get_eq_getElem,
+    getElem_toArray, getElem_cons_succ]
+  split
+  rw [takeWhile_go_succ]
+  rfl
+
+theorem takeWhile_go_toArray (p : α → Bool) (l : List α) (i : Nat) :
+    Array.takeWhile.go p l.toArray i r = r ++ (takeWhile p (l.drop i)).toArray := by
+  induction l generalizing i r with
+  | nil => simp [takeWhile.go]
+  | cons a l ih =>
+    rw [takeWhile.go]
+    cases i with
+    | zero =>
+      simp [takeWhile_go_succ, ih, takeWhile_cons]
+      split <;> simp
+    | succ i =>
+      simp only [size_toArray, length_cons, Nat.add_lt_add_iff_right, Array.get_eq_getElem,
+        getElem_toArray, getElem_cons_succ, drop_succ_cons]
+      split <;> rename_i h₁
+      · rw [takeWhile_go_succ, ih]
+        rw [← getElem_cons_drop_succ_eq_drop h₁, takeWhile_cons]
+        split <;> simp_all
+      · simp_all [drop_eq_nil_of_le]
+
+@[simp] theorem takeWhile_toArray (p : α → Bool) (l : List α) :
+    l.toArray.takeWhile p = (l.takeWhile p).toArray := by
+  simp [Array.takeWhile, takeWhile_go_toArray]
+
+@[simp] theorem setIfInBounds_toArray (l : List α) (i : Nat) (a : α) :
+    l.toArray.setIfInBounds i a  = (l.set i a).toArray := by
+  apply ext'
+  simp only [setIfInBounds]
+  split
+  · simp
+  · simp_all [List.set_eq_of_length_le]
+
+end List

src/Init/Data/List/ToArrayImpl.lean

@@ -0,0 +1,23 @@
+/-
+Copyright (c) 2024 Lean FRO. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+prelude
+import Init.Data.List.Basic
+
+/--
+Auxiliary definition for `List.toArray`.
+`List.toArrayAux as r = r ++ as.toArray`
+-/
+@[inline_if_reduce]
+def List.toArrayAux : List α → Array α → Array α
+  | nil,       r => r
+  | cons a as, r => toArrayAux as (r.push a)
+
+/-- Convert a `List α` into an `Array α`. This is O(n) in the length of the list.  -/
+-- This function is exported to C, where it is called by `Array.mk`
+-- (the constructor) to implement this functionality.
+@[inline, match_pattern, pp_nodot, export lean_list_to_array]
+def List.toArrayImpl (as : List α) : Array α :=
+  as.toArrayAux (Array.mkEmpty as.length)

src/Init/Data/Nat/Lemmas.lean

@@ -1046,6 +1046,25 @@ instance decidableExistsLE [DecidablePred p] : DecidablePred fun n => ∃ m : Na
   fun n => decidable_of_iff (∃ m, m < n + 1 ∧ p m)
     (exists_congr fun _ => and_congr_left' Nat.lt_succ_iff)
 
+/-- Dependent version of `decidableExistsLT`. -/
+instance decidableExistsLT' {p : (m : Nat) → m < k → Prop} [I : ∀ m h, Decidable (p m h)] :
+    Decidable (∃ m : Nat, ∃ h : m < k, p m h) :=
+  match k, p, I with
+  | 0, _, _ => isFalse (by simp)
+  | (k + 1), p, I => @decidable_of_iff _ ((∃ m, ∃ h : m < k, p m (by omega)) ∨ p k (by omega))
+      ⟨by rintro (⟨m, h, w⟩ | w); exact ⟨m, by omega, w⟩; exact ⟨k, by omega, w⟩,
+        fun ⟨m, h, w⟩ => if h' : m < k then .inl ⟨m, h', w⟩ else
+          by obtain rfl := (by omega : m = k); exact .inr w⟩
+      (@instDecidableOr _ _
+        (decidableExistsLT' (p := fun m h => p m (by omega)) (I := fun m h => I m (by omega)))
+        inferInstance)
+
+/-- Dependent version of `decidableExistsLE`. -/
+instance decidableExistsLE' {p : (m : Nat) → m ≤ k → Prop} [I : ∀ m h, Decidable (p m h)] :
+    Decidable (∃ m : Nat, ∃ h : m ≤ k, p m h) :=
+  decidable_of_iff (∃ m, ∃ h : m < k + 1, p m (by omega)) (exists_congr fun _ =>
+    ⟨fun ⟨h, w⟩ => ⟨le_of_lt_succ h, w⟩, fun ⟨h, w⟩ => ⟨lt_add_one_of_le h, w⟩⟩)
+
 /-! ### Results about `List.sum` specialized to `Nat` -/
 
 protected theorem sum_pos_iff_exists_pos {l : List Nat} : 0 < l.sum ↔ ∃ x ∈ l, 0 < x := by

src/Init/GetElem.lean

@@ -118,12 +118,16 @@ instance (priority := low) [GetElem coll idx elem valid] [∀ xs i, Decidable (v
     GetElem? coll idx elem valid where
   getElem? xs i := decidableGetElem? xs i
 
-theorem getElem_congr_coll [GetElem coll idx elem valid] {c d : coll} {i : idx} {h : valid c i}
-    (h' : c = d) : c[i] = d[i]'(h' ▸ h) := by
-  cases h'; rfl
+theorem getElem_congr [GetElem coll idx elem valid] {c d : coll} (h : c = d)
+    {i j : idx} (h' : i = j) (w : valid c i) : c[i] = d[j]'(h' ▸ h ▸ w) := by
+  cases h; cases h'; rfl
 
-theorem getElem_congr [GetElem coll idx elem valid] {c : coll} {i j : idx} {h : valid c i}
-    (h' : i = j) : c[i] = c[j]'(h' ▸ h) := by
+theorem getElem_congr_coll [GetElem coll idx elem valid] {c d : coll} {i : idx} {w : valid c i}
+    (h : c = d) : c[i] = d[i]'(h ▸ w) := by
+  cases h; rfl
+
+theorem getElem_congr_idx [GetElem coll idx elem valid] {c : coll} {i j : idx} {w : valid c i}
+    (h' : i = j) : c[i] = c[j]'(h' ▸ w) := by
   cases h'; rfl
 
 class LawfulGetElem (cont : Type u) (idx : Type v) (elem : outParam (Type w))
@@ -216,13 +220,9 @@ instance : GetElem (List α) Nat α fun as i => i < as.length where
 @[simp] theorem getElem_cons_zero (a : α) (as : List α) (h : 0 < (a :: as).length) : getElem (a :: as) 0 h = a := by
   rfl
 
-@[deprecated getElem_cons_zero (since := "2024-06-12")] abbrev cons_getElem_zero := @getElem_cons_zero
-
 @[simp] theorem getElem_cons_succ (a : α) (as : List α) (i : Nat) (h : i + 1 < (a :: as).length) : getElem (a :: as) (i+1) h = getElem as i (Nat.lt_of_succ_lt_succ h) := by
   rfl
 
-@[deprecated getElem_cons_succ (since := "2024-06-12")] abbrev cons_getElem_succ := @getElem_cons_succ
-
 @[simp] theorem getElem_mem : ∀ {l : List α} {n} (h : n < l.length), l[n]'h ∈ l
   | _ :: _, 0, _ => .head ..
   | _ :: l, _+1, _ => .tail _ (getElem_mem (l := l) ..)
@@ -243,6 +243,12 @@ namespace Array
 instance : GetElem (Array α) Nat α fun xs i => i < xs.size where
   getElem xs i h := xs.get i h
 
+@[simp] theorem get_eq_getElem (a : Array α) (i : Nat) (h) : a.get i h = a[i] := rfl
+
+@[simp] theorem get!_eq_getElem! [Inhabited α] (a : Array α) (i : Nat) : a.get! i = a[i]! := by
+  simp only [get!, getD, get_eq_getElem, getElem!_def]
+  split <;> simp_all [getElem?_pos, getElem?_neg]
+
 end Array
 
 namespace Lean.Syntax

src/Init/Meta.lean

@@ -679,6 +679,7 @@ private partial def decodeBinLitAux (s : String) (i : String.Pos) (val : Nat) :
     let c := s.get i
     if c == '0' then decodeBinLitAux s (s.next i) (2*val)
     else if c == '1' then decodeBinLitAux s (s.next i) (2*val + 1)
+    else if c == '_' then decodeBinLitAux s (s.next i) val
     else none
 
 private partial def decodeOctalLitAux (s : String) (i : String.Pos) (val : Nat) : Option Nat :=
@@ -686,6 +687,7 @@ private partial def decodeOctalLitAux (s : String) (i : String.Pos) (val : Nat)
   else
     let c := s.get i
     if '0' ≤ c && c ≤ '7' then decodeOctalLitAux s (s.next i) (8*val + c.toNat - '0'.toNat)
+    else if c == '_' then decodeOctalLitAux s (s.next i) val
     else none
 
 private def decodeHexDigit (s : String) (i : String.Pos) : Option (Nat × String.Pos) :=
@@ -700,13 +702,16 @@ private partial def decodeHexLitAux (s : String) (i : String.Pos) (val : Nat) :
   if s.atEnd i then some val
   else match decodeHexDigit s i with
     | some (d, i) => decodeHexLitAux s i (16*val + d)
-    | none        => none
+    | none        =>
+      if s.get i == '_' then decodeHexLitAux s (s.next i) val
+      else none
 
 private partial def decodeDecimalLitAux (s : String) (i : String.Pos) (val : Nat) : Option Nat :=
   if s.atEnd i then some val
   else
     let c := s.get i
     if '0' ≤ c && c ≤ '9' then decodeDecimalLitAux s (s.next i) (10*val + c.toNat - '0'.toNat)
+    else if c == '_' then decodeDecimalLitAux s (s.next i) val
     else none
 
 def decodeNatLitVal? (s : String) : Option Nat :=
@@ -773,6 +778,8 @@ where
       let c := s.get i
       if '0' ≤ c && c ≤ '9' then
         decodeAfterExp (s.next i) val e sign (10*exp + c.toNat - '0'.toNat)
+      else if c == '_' then
+        decodeAfterExp (s.next i) val e sign exp
       else
         none
 
@@ -793,6 +800,8 @@ where
       let c := s.get i
       if '0' ≤ c && c ≤ '9' then
         decodeAfterDot (s.next i) (10*val + c.toNat - '0'.toNat) (e+1)
+      else if c == '_' then
+        decodeAfterDot (s.next i) val e
       else if c == 'e' || c == 'E' then
         decodeExp (s.next i) val e
       else
@@ -805,6 +814,8 @@ where
       let c := s.get i
       if '0' ≤ c && c ≤ '9' then
         decode (s.next i) (10*val + c.toNat - '0'.toNat)
+      else if c == '_' then
+        decode (s.next i) val
       else if c == '.' then
         decodeAfterDot (s.next i) val 0
       else if c == 'e' || c == 'E' then

src/Init/PropLemmas.lean

@@ -386,6 +386,15 @@ theorem exists_comm {p : α → β → Prop} : (∃ a b, p a b) ↔ (∃ b a, p
 theorem forall_prop_of_false {p : Prop} {q : p → Prop} (hn : ¬p) : (∀ h' : p, q h') ↔ True :=
   iff_true_intro fun h => hn.elim h
 
+@[simp] theorem and_exists_self (P : Prop) (Q : P → Prop) : (P ∧ ∃ p, Q p) ↔ ∃ p, Q p :=
+  ⟨fun ⟨_, h⟩ => h, fun ⟨p, q⟩ => ⟨p, ⟨p, q⟩⟩⟩
+
+@[simp] theorem exists_and_self (P : Prop) (Q : P → Prop) : ((∃ p, Q p) ∧ P) ↔ ∃ p, Q p :=
+  ⟨fun ⟨h, _⟩ => h, fun ⟨p, q⟩ => ⟨⟨p, q⟩, p⟩⟩
+
+@[simp] theorem forall_self_imp (P : Prop) (Q : P → Prop) : (∀ p : P, P → Q p) ↔ ∀ p, Q p :=
+  ⟨fun h p => h p p, fun h _ p => h p⟩
+
 end quantifiers
 
 /-! ## membership -/

src/Lean/Compiler/IR/Basic.lean

@@ -81,6 +81,7 @@ then one of the following must hold in each (execution) branch.
 inductive IRType where
   | float | uint8 | uint16 | uint32 | uint64 | usize
   | irrelevant | object | tobject
+  | float32
   | struct (leanTypeName : Option Name) (types : Array IRType) : IRType
   | union (leanTypeName : Name) (types : Array IRType) : IRType
   deriving Inhabited, Repr
@@ -89,6 +90,7 @@ namespace IRType
 
 partial def beq : IRType → IRType → Bool
   | float,          float          => true
+  | float32,        float32        => true
   | uint8,          uint8          => true
   | uint16,         uint16         => true
   | uint32,         uint32         => true
@@ -104,13 +106,14 @@ partial def beq : IRType → IRType → Bool
 instance : BEq IRType := ⟨beq⟩
 
 def isScalar : IRType → Bool
-  | float  => true
-  | uint8  => true
-  | uint16 => true
-  | uint32 => true
-  | uint64 => true
-  | usize  => true
-  | _      => false
+  | float    => true
+  | float32  => true
+  | uint8    => true
+  | uint16   => true
+  | uint32   => true
+  | uint64   => true
+  | usize    => true
+  | _        => false
 
 def isObj : IRType → Bool
   | object  => true
@@ -611,10 +614,11 @@ def mkIf (x : VarId) (t e : FnBody) : FnBody :=
 
 def getUnboxOpName (t : IRType) : String :=
   match t with
-  | IRType.usize  => "lean_unbox_usize"
-  | IRType.uint32 => "lean_unbox_uint32"
-  | IRType.uint64 => "lean_unbox_uint64"
-  | IRType.float  => "lean_unbox_float"
-  | _             => "lean_unbox"
+  | IRType.usize    => "lean_unbox_usize"
+  | IRType.uint32   => "lean_unbox_uint32"
+  | IRType.uint64   => "lean_unbox_uint64"
+  | IRType.float    => "lean_unbox_float"
+  | IRType.float32  => "lean_unbox_float32"
+  | _               => "lean_unbox"
 
 end Lean.IR

src/Lean/Compiler/IR/EmitC.lean

@@ -55,6 +55,7 @@ def emitArg (x : Arg) : M Unit :=
 
 def toCType : IRType → String
   | IRType.float      => "double"
+  | IRType.float32    => "float"
   | IRType.uint8      => "uint8_t"
   | IRType.uint16     => "uint16_t"
   | IRType.uint32     => "uint32_t"
@@ -311,12 +312,13 @@ def emitUSet (x : VarId) (n : Nat) (y : VarId) : M Unit := do
 
 def emitSSet (x : VarId) (n : Nat) (offset : Nat) (y : VarId) (t : IRType) : M Unit := do
   match t with
-  | IRType.float  => emit "lean_ctor_set_float"
-  | IRType.uint8  => emit "lean_ctor_set_uint8"
-  | IRType.uint16 => emit "lean_ctor_set_uint16"
-  | IRType.uint32 => emit "lean_ctor_set_uint32"
-  | IRType.uint64 => emit "lean_ctor_set_uint64"
-  | _             => throw "invalid instruction";
+  | IRType.float   => emit "lean_ctor_set_float"
+  | IRType.float32 => emit "lean_ctor_set_float32"
+  | IRType.uint8   => emit "lean_ctor_set_uint8"
+  | IRType.uint16  => emit "lean_ctor_set_uint16"
+  | IRType.uint32  => emit "lean_ctor_set_uint32"
+  | IRType.uint64  => emit "lean_ctor_set_uint64"
+  | _              => throw "invalid instruction";
   emit "("; emit x; emit ", "; emitOffset n offset; emit ", "; emit y; emitLn ");"
 
 def emitJmp (j : JoinPointId) (xs : Array Arg) : M Unit := do
@@ -386,12 +388,13 @@ def emitUProj (z : VarId) (i : Nat) (x : VarId) : M Unit := do
 def emitSProj (z : VarId) (t : IRType) (n offset : Nat) (x : VarId) : M Unit := do
   emitLhs z;
   match t with
-  | IRType.float  => emit "lean_ctor_get_float"
-  | IRType.uint8  => emit "lean_ctor_get_uint8"
-  | IRType.uint16 => emit "lean_ctor_get_uint16"
-  | IRType.uint32 => emit "lean_ctor_get_uint32"
-  | IRType.uint64 => emit "lean_ctor_get_uint64"
-  | _             => throw "invalid instruction"
+  | IRType.float    => emit "lean_ctor_get_float"
+  | IRType.float32  => emit "lean_ctor_get_float32"
+  | IRType.uint8    => emit "lean_ctor_get_uint8"
+  | IRType.uint16   => emit "lean_ctor_get_uint16"
+  | IRType.uint32   => emit "lean_ctor_get_uint32"
+  | IRType.uint64   => emit "lean_ctor_get_uint64"
+  | _               => throw "invalid instruction"
   emit "("; emit x; emit ", "; emitOffset n offset; emitLn ");"
 
 def toStringArgs (ys : Array Arg) : List String :=
@@ -446,11 +449,12 @@ def emitApp (z : VarId) (f : VarId) (ys : Array Arg) : M Unit :=
 
 def emitBoxFn (xType : IRType) : M Unit :=
   match xType with
-  | IRType.usize  => emit "lean_box_usize"
-  | IRType.uint32 => emit "lean_box_uint32"
-  | IRType.uint64 => emit "lean_box_uint64"
-  | IRType.float  => emit "lean_box_float"
-  | _             => emit "lean_box"
+  | IRType.usize   => emit "lean_box_usize"
+  | IRType.uint32  => emit "lean_box_uint32"
+  | IRType.uint64  => emit "lean_box_uint64"
+  | IRType.float   => emit "lean_box_float"
+  | IRType.float32 => emit "lean_box_float32"
+  | _              => emit "lean_box"
 
 def emitBox (z : VarId) (x : VarId) (xType : IRType) : M Unit := do
   emitLhs z; emitBoxFn xType; emit "("; emit x; emitLn ");"

src/Lean/Compiler/IR/EmitLLVM.lean

@@ -315,6 +315,7 @@ def callLeanCtorSetTag (builder : LLVM.Builder llvmctx)
 def toLLVMType (t : IRType) : M llvmctx (LLVM.LLVMType llvmctx) := do
   match t with
   | IRType.float      => LLVM.doubleTypeInContext llvmctx
+  | IRType.float32    => LLVM.floatTypeInContext llvmctx
   | IRType.uint8      => LLVM.intTypeInContext llvmctx 8
   | IRType.uint16     => LLVM.intTypeInContext llvmctx 16
   | IRType.uint32     => LLVM.intTypeInContext llvmctx 32
@@ -817,12 +818,13 @@ def emitSProj (builder : LLVM.Builder llvmctx)
     (z : VarId) (t : IRType) (n offset : Nat) (x : VarId) : M llvmctx Unit := do
   let (fnName, retty) ←
     match t with
-    | IRType.float  => pure ("lean_ctor_get_float", ← LLVM.doubleTypeInContext llvmctx)
-    | IRType.uint8  => pure ("lean_ctor_get_uint8", ← LLVM.i8Type llvmctx)
-    | IRType.uint16 => pure ("lean_ctor_get_uint16", ←  LLVM.i16Type llvmctx)
-    | IRType.uint32 => pure ("lean_ctor_get_uint32", ← LLVM.i32Type llvmctx)
-    | IRType.uint64 => pure ("lean_ctor_get_uint64", ← LLVM.i64Type llvmctx)
-    | _             => throw s!"Invalid type for lean_ctor_get: '{t}'"
+    | IRType.float   => pure ("lean_ctor_get_float", ← LLVM.doubleTypeInContext llvmctx)
+    | IRType.float32 => pure ("lean_ctor_get_float32", ← LLVM.floatTypeInContext llvmctx)
+    | IRType.uint8   => pure ("lean_ctor_get_uint8", ← LLVM.i8Type llvmctx)
+    | IRType.uint16  => pure ("lean_ctor_get_uint16", ←  LLVM.i16Type llvmctx)
+    | IRType.uint32  => pure ("lean_ctor_get_uint32", ← LLVM.i32Type llvmctx)
+    | IRType.uint64  => pure ("lean_ctor_get_uint64", ← LLVM.i64Type llvmctx)
+    | _              => throw s!"Invalid type for lean_ctor_get: '{t}'"
   let argtys := #[ ← LLVM.voidPtrType llvmctx, ← LLVM.unsignedType llvmctx]
   let fn ← getOrCreateFunctionPrototype (← getLLVMModule) retty fnName argtys
   let xval ← emitLhsVal builder x
@@ -862,11 +864,12 @@ def emitBox (builder : LLVM.Builder llvmctx) (z : VarId) (x : VarId) (xType : IR
   let xv ← emitLhsVal builder x
   let (fnName, argTy, xv) ←
     match xType with
-    | IRType.usize  => pure ("lean_box_usize", ← LLVM.size_tType llvmctx, xv)
-    | IRType.uint32 => pure ("lean_box_uint32", ← LLVM.i32Type llvmctx, xv)
-    | IRType.uint64 => pure ("lean_box_uint64", ← LLVM.size_tType llvmctx, xv)
-    | IRType.float  => pure ("lean_box_float", ← LLVM.doubleTypeInContext llvmctx, xv)
-    | _             => do
+    | IRType.usize   => pure ("lean_box_usize", ← LLVM.size_tType llvmctx, xv)
+    | IRType.uint32  => pure ("lean_box_uint32", ← LLVM.i32Type llvmctx, xv)
+    | IRType.uint64  => pure ("lean_box_uint64", ← LLVM.size_tType llvmctx, xv)
+    | IRType.float   => pure ("lean_box_float", ← LLVM.doubleTypeInContext llvmctx, xv)
+    | IRType.float32 => pure ("lean_box_float32", ← LLVM.floatTypeInContext llvmctx, xv)
+    | _              =>
          -- sign extend smaller values into i64
          let xv ← LLVM.buildSext builder xv (← LLVM.size_tType llvmctx)
          pure ("lean_box", ← LLVM.size_tType llvmctx, xv)
@@ -892,11 +895,12 @@ def callUnboxForType (builder : LLVM.Builder llvmctx)
     (retName : String := "") : M llvmctx (LLVM.Value llvmctx) := do
   let (fnName, retty) ←
      match t with
-     | IRType.usize  => pure ("lean_unbox_usize", ← toLLVMType t)
-     | IRType.uint32 => pure ("lean_unbox_uint32", ← toLLVMType t)
-     | IRType.uint64 => pure ("lean_unbox_uint64", ← toLLVMType t)
-     | IRType.float  => pure ("lean_unbox_float", ← toLLVMType t)
-     | _             => pure ("lean_unbox", ← LLVM.size_tType llvmctx)
+     | IRType.usize   => pure ("lean_unbox_usize", ← toLLVMType t)
+     | IRType.uint32  => pure ("lean_unbox_uint32", ← toLLVMType t)
+     | IRType.uint64  => pure ("lean_unbox_uint64", ← toLLVMType t)
+     | IRType.float   => pure ("lean_unbox_float", ← toLLVMType t)
+     | IRType.float32 => pure ("lean_unbox_float32", ← toLLVMType t)
+     | _              => pure ("lean_unbox", ← LLVM.size_tType llvmctx)
   let argtys := #[← LLVM.voidPtrType llvmctx ]
   let fn ← getOrCreateFunctionPrototype (← getLLVMModule) retty fnName argtys
   let fnty ← LLVM.functionType retty argtys
@@ -1041,12 +1045,13 @@ def emitJmp (builder : LLVM.Builder llvmctx) (jp : JoinPointId) (xs : Array Arg)
 def emitSSet (builder : LLVM.Builder llvmctx) (x : VarId) (n : Nat) (offset : Nat) (y : VarId) (t : IRType) : M llvmctx Unit := do
   let (fnName, setty) ←
   match t with
-  | IRType.float  => pure ("lean_ctor_set_float", ← LLVM.doubleTypeInContext llvmctx)
-  | IRType.uint8  => pure ("lean_ctor_set_uint8", ← LLVM.i8Type llvmctx)
-  | IRType.uint16 => pure ("lean_ctor_set_uint16", ← LLVM.i16Type llvmctx)
-  | IRType.uint32 => pure ("lean_ctor_set_uint32", ← LLVM.i32Type llvmctx)
-  | IRType.uint64 => pure ("lean_ctor_set_uint64", ← LLVM.i64Type llvmctx)
-  | _             => throw s!"invalid type for 'lean_ctor_set': '{t}'"
+  | IRType.float   => pure ("lean_ctor_set_float", ← LLVM.doubleTypeInContext llvmctx)
+  | IRType.float32 => pure ("lean_ctor_set_float32", ← LLVM.floatTypeInContext llvmctx)
+  | IRType.uint8   => pure ("lean_ctor_set_uint8", ← LLVM.i8Type llvmctx)
+  | IRType.uint16  => pure ("lean_ctor_set_uint16", ← LLVM.i16Type llvmctx)
+  | IRType.uint32  => pure ("lean_ctor_set_uint32", ← LLVM.i32Type llvmctx)
+  | IRType.uint64  => pure ("lean_ctor_set_uint64", ← LLVM.i64Type llvmctx)
+  | _              => throw s!"invalid type for 'lean_ctor_set': '{t}'"
   let argtys := #[ ← LLVM.voidPtrType llvmctx, ← LLVM.unsignedType llvmctx, setty]
   let retty  ← LLVM.voidType llvmctx
   let fn ← getOrCreateFunctionPrototype (← getLLVMModule) retty fnName argtys

src/Lean/Compiler/IR/Format.lean

@@ -55,6 +55,7 @@ instance : ToString Expr := ⟨fun e => Format.pretty (format e)⟩
 
 private partial def formatIRType : IRType → Format
   | IRType.float        => "float"
+  | IRType.float32      => "float32"
   | IRType.uint8        => "u8"
   | IRType.uint16       => "u16"
   | IRType.uint32       => "u32"

src/Lean/Elab/PreDefinition/Main.lean

@@ -22,7 +22,8 @@ private def addAndCompilePartial (preDefs : Array PreDefinition) (useSorry := fa
       let value ← if useSorry then
         mkLambdaFVars xs (← mkSorry type (synthetic := true))
       else
-        liftM <| mkInhabitantFor preDef.declName xs type
+        let msg := m!"failed to compile 'partial' definition '{preDef.declName}'"
+        liftM <| mkInhabitantFor msg xs type
       addNonRec { preDef with
         kind  := DefKind.«opaque»
         value

src/Lean/Elab/PreDefinition/MkInhabitant.lean

@@ -50,13 +50,13 @@ private partial def mkInhabitantForAux? (xs insts : Array Expr) (type : Expr) (u
       return none
 
 /- TODO: add a global IO.Ref to let users customize/extend this procedure -/
-def mkInhabitantFor (declName : Name) (xs : Array Expr) (type : Expr) : MetaM Expr :=
+def mkInhabitantFor (failedToMessage : MessageData) (xs : Array Expr) (type : Expr) : MetaM Expr :=
   withInhabitedInstances xs fun insts => do
     if let some val ← mkInhabitantForAux? xs insts type false <||> mkInhabitantForAux? xs insts type true then
       return val
     else
       throwError "\
-        failed to compile 'partial' definition '{declName}', could not prove that the type\
+        {failedToMessage}, could not prove that the type\
         {indentExpr (← mkForallFVars xs type)}\n\
         is nonempty.\n\
         \n\

src/Lean/Elab/PreDefinition/WF/Eqns.lean

@@ -20,6 +20,7 @@ structure EqnInfo extends EqnInfoCore where
   declNameNonRec  : Name
   fixedPrefixSize : Nat
   argsPacker      : ArgsPacker
+  hasInduct       : Bool
   deriving Inhabited
 
 private partial def deltaLHSUntilFix (mvarId : MVarId) : MetaM MVarId := mvarId.withContext do
@@ -101,7 +102,7 @@ def mkEqns (declName : Name) (info : EqnInfo) : MetaM (Array Name) :=
 builtin_initialize eqnInfoExt : MapDeclarationExtension EqnInfo ← mkMapDeclarationExtension
 
 def registerEqnsInfo (preDefs : Array PreDefinition) (declNameNonRec : Name) (fixedPrefixSize : Nat)
-    (argsPacker : ArgsPacker) : MetaM Unit := do
+    (argsPacker : ArgsPacker) (hasInduct : Bool) : MetaM Unit := do
   preDefs.forM fun preDef => ensureEqnReservedNamesAvailable preDef.declName
   /-
   See issue #2327.
@@ -114,7 +115,7 @@ def registerEqnsInfo (preDefs : Array PreDefinition) (declNameNonRec : Name) (fi
       modifyEnv fun env =>
         preDefs.foldl (init := env) fun env preDef =>
           eqnInfoExt.insert env preDef.declName { preDef with
-            declNames, declNameNonRec, fixedPrefixSize, argsPacker }
+            declNames, declNameNonRec, fixedPrefixSize, argsPacker, hasInduct }
 
 def getEqnsFor? (declName : Name) : MetaM (Option (Array Name)) := do
   if let some info := eqnInfoExt.find? (← getEnv) declName then

src/Lean/Elab/PreDefinition/WF/Fix.lean

@@ -178,7 +178,8 @@ def groupGoalsByFunction (argsPacker : ArgsPacker) (numFuncs : Nat) (goals : Arr
     let type ← goal.getType
     let (.mdata _ (.app _ param)) := type
         | throwError "MVar does not look like a recursive call:{indentExpr type}"
-    let (funidx, _) ← argsPacker.unpack param
+    let some (funidx, _) := argsPacker.unpack param
+        | throwError "Cannot unpack param, unexpected expression:{indentExpr param}"
     r := r.modify funidx (·.push goal)
   return r
 

src/Lean/Elab/PreDefinition/WF/GuessLex.lean

@@ -352,8 +352,10 @@ def collectRecCalls (unaryPreDef : PreDefinition) (fixedPrefixSize : Nat)
         throwError "Insufficient arguments in recursive call"
       let arg := args[fixedPrefixSize]!
       trace[Elab.definition.wf] "collectRecCalls: {unaryPreDef.declName} ({param}) → {unaryPreDef.declName} ({arg})"
-      let (caller, params) ← argsPacker.unpack param
-      let (callee, args) ← argsPacker.unpack arg
+      let some (caller, params) := argsPacker.unpack param
+        | throwError "Cannot unpack param, unexpected expression:{indentExpr param}"
+      let some (callee, args) := argsPacker.unpack arg
+        | throwError "Cannot unpack arg, unexpected expression:{indentExpr arg}"
       RecCallWithContext.create (← getRef) caller (ys ++ params) callee (ys ++ args)
 
 /-- Is the expression a `<`-like comparison of `Nat` expressions -/
@@ -771,6 +773,8 @@ Main entry point of this module:
 
 Try to find a lexicographic ordering of the arguments for which the recursive definition
 terminates. See the module doc string for a high-level overview.
+
+The `preDefs` are used to determine arity and types of arguments; the bodies are ignored.
 -/
 def guessLex (preDefs : Array PreDefinition) (unaryPreDef : PreDefinition)
     (fixedPrefixSize : Nat) (argsPacker : ArgsPacker) :

src/Lean/Elab/PreDefinition/WF/Main.lean

@@ -110,7 +110,7 @@ def wfRecursion (preDefs : Array PreDefinition) (termArg?s : Array (Option Termi
     unless type.isForall do
       throwError "wfRecursion: expected unary function type: {type}"
     let packedArgType := type.bindingDomain!
-    elabWFRel preDefs unaryPreDef.declName prefixArgs argsPacker packedArgType wf fun wfRel => do
+    elabWFRel (preDefs.map (·.declName)) unaryPreDef.declName prefixArgs argsPacker packedArgType wf fun wfRel => do
       trace[Elab.definition.wf] "wfRel: {wfRel}"
       let (value, envNew) ← withoutModifyingEnv' do
         addAsAxiom unaryPreDef
@@ -142,7 +142,7 @@ def wfRecursion (preDefs : Array PreDefinition) (termArg?s : Array (Option Termi
   -- Reason: the nested proofs may be referring to the _unsafe_rec.
   addAndCompilePartialRec preDefs
   let preDefs ← preDefs.mapM (abstractNestedProofs ·)
-  registerEqnsInfo preDefs preDefNonRec.declName fixedPrefixSize argsPacker
+  registerEqnsInfo preDefs preDefNonRec.declName fixedPrefixSize argsPacker (hasInduct := true)
   for preDef in preDefs do
     markAsRecursive preDef.declName
     generateEagerEqns preDef.declName

src/Lean/Elab/PreDefinition/WF/Rel.lean

@@ -51,12 +51,12 @@ If the `termArgs` map the packed argument `argType` to `β`, then this function
 continuation a value of type `WellFoundedRelation argType` that is derived from the instance
 for `WellFoundedRelation β` using `invImage`.
 -/
-def elabWFRel (preDefs : Array PreDefinition) (unaryPreDefName : Name) (prefixArgs : Array Expr)
+def elabWFRel (declNames : Array Name) (unaryPreDefName : Name) (prefixArgs : Array Expr)
     (argsPacker : ArgsPacker) (argType : Expr) (termArgs : TerminationArguments)
     (k : Expr → TermElabM α) : TermElabM α := withDeclName unaryPreDefName do
   let α := argType
   let u ← getLevel α
-  let β ← checkCodomains (preDefs.map (·.declName)) prefixArgs argsPacker.arities termArgs
+  let β ← checkCodomains declNames prefixArgs argsPacker.arities termArgs
   let v ← getLevel β
   let packedF ← argsPacker.uncurryND (termArgs.map (·.fn.beta prefixArgs))
   let inst ← synthInstance (.app (.const ``WellFoundedRelation [v]) β)

src/Lean/Expr.lean

@@ -1235,6 +1235,9 @@ def getRevArg!' : Expr → Nat → Expr
 @[inline] def getArgD (e : Expr) (i : Nat) (v₀ : Expr) (n := e.getAppNumArgs) : Expr :=
   getRevArgD e (n - i - 1) v₀
 
+/-- Return `true` if `e` contains any loose bound variables.
+
+This is a constant time operation. -/
 def hasLooseBVars (e : Expr) : Bool :=
   e.looseBVarRange > 0
 
@@ -1247,6 +1250,11 @@ def isArrow (e : Expr) : Bool :=
   | forallE _ _ b _ => !b.hasLooseBVars
   | _ => false
 
+/--
+Return `true` if `e` contains the specified loose bound variable with index `bvarIdx`.
+
+This operation traverses the expression tree.
+-/
 @[extern "lean_expr_has_loose_bvar"]
 opaque hasLooseBVar (e : @& Expr) (bvarIdx : @& Nat) : Bool
 

src/Lean/Meta/ArgsPacker.lean

@@ -87,7 +87,7 @@ Unpacks a unary packed argument created with `Unary.pack`.
 
 Throws an error if the expression is not of that form.
 -/
-def unpack (arity : Nat) (e : Expr) : MetaM (Array Expr) := do
+def unpack (arity : Nat) (e : Expr) : Option (Array Expr) := do
   let mut e := e
   let mut args := #[]
   while args.size + 1 < arity do
@@ -95,11 +95,10 @@ def unpack (arity : Nat) (e : Expr) : MetaM (Array Expr) := do
       args := args.push (e.getArg! 2)
       e := e.getArg! 3
     else
-      throwError "Unexpected expression while unpacking n-ary argument"
+      none
   args := args.push e
   return args
 
-
 /--
   Given a (dependent) tuple `t` (using `PSigma`) of the given arity.
   Return an array containing its "elements".
@@ -258,7 +257,7 @@ argument and function index.
 
 Throws an error if the expression is not of that form.
 -/
-def unpack (numFuncs : Nat) (expr : Expr) : MetaM (Nat × Expr) := do
+def unpack (numFuncs : Nat) (expr : Expr) : Option (Nat × Expr) := do
   let mut funidx := 0
   let mut e := expr
   while funidx + 1 < numFuncs do
@@ -269,7 +268,7 @@ def unpack (numFuncs : Nat) (expr : Expr) : MetaM (Nat × Expr) := do
       e := e.getArg! 2
       break
     else
-      throwError "Unexpected expression while unpacking mutual argument:{indentExpr expr}"
+      none
   return (funidx, e)
 
 
@@ -377,14 +376,17 @@ and `(z : C) → R₂[z]`, returns an expression of type
 (x : A ⊕' C) → (match x with | .inl x => R₁[x] | .inr R₂[z])
 ```
 -/
-def uncurry (es : Array Expr) : MetaM Expr := do
-  let types ← es.mapM inferType
-  let resultType ← uncurryType types
+def uncurryWithType (resultType : Expr) (es : Array Expr) : MetaM Expr := do
   forallBoundedTelescope resultType (some 1) fun xs codomain => do
     let #[x] := xs | unreachable!
     let value ← casesOn x codomain es.toList
     mkLambdaFVars #[x] value
 
+def uncurry (es : Array Expr) : MetaM Expr := do
+  let types ← es.mapM inferType
+  let resultType ← uncurryType types
+  uncurryWithType resultType es
+
 /--
 Given unary expressions `e₁`, `e₂` with types `(x : A) → R`
 and `(z : C) → R`, returns an expression of type
@@ -414,7 +416,7 @@ def curryType (n : Nat) (type : Expr) : MetaM (Array Expr) := do
 
 end Mutual
 
--- Now for the main definitions in this moduleo
+-- Now for the main definitions in this module
 
 /-- The number of functions being packed -/
 def numFuncs (argsPacker : ArgsPacker) : Nat := argsPacker.varNamess.size
@@ -422,6 +424,10 @@ def numFuncs (argsPacker : ArgsPacker) : Nat := argsPacker.varNamess.size
 /-- The arities of the functions being packed -/
 def arities (argsPacker : ArgsPacker) : Array Nat := argsPacker.varNamess.map (·.size)
 
+def onlyOneUnary (argsPacker : ArgsPacker) :=
+  argsPacker.varNamess.size = 1 &&
+  argsPacker.varNamess[0]!.size = 1
+
 def pack (argsPacker : ArgsPacker) (domain : Expr) (fidx : Nat) (args : Array Expr)
     : MetaM Expr := do
   assert! fidx < argsPacker.numFuncs
@@ -436,14 +442,13 @@ return the function index that is called and the arguments individually.
 
 We expect precisely the expressions produced by `pack`, with manifest
 `PSum.inr`, `PSum.inl` and `PSigma.mk` constructors, and thus take them apart
-rather than using projectinos.
+rather than using projections.
 -/
-def unpack (argsPacker : ArgsPacker) (e : Expr) : MetaM (Nat × Array Expr) := do
+def unpack (argsPacker : ArgsPacker) (e : Expr) : Option (Nat × Array Expr) := do
   let (funidx, e) ← Mutual.unpack argsPacker.numFuncs e
   let args ← Unary.unpack argsPacker.varNamess[funidx]!.size e
   return (funidx, args)
 
-
 /--
 Given types `(x : A) → (y : B[x]) → R₁[x,y]` and `(z : C) → R₂[z]`, returns the type uncurried type
 ```
@@ -465,6 +470,10 @@ def uncurry (argsPacker : ArgsPacker) (es : Array Expr) : MetaM Expr := do
   let unary ← (Array.zipWith argsPacker.varNamess es Unary.uncurry).mapM id
   Mutual.uncurry unary
 
+def uncurryWithType (argsPacker : ArgsPacker) (resultType : Expr) (es : Array Expr) : MetaM Expr := do
+  let unary ← (Array.zipWith argsPacker.varNamess es Unary.uncurry).mapM id
+  Mutual.uncurryWithType resultType unary
+
 /--
 Given expressions `e₁`, `e₂` with types `(x : A) → (y : B[x]) → R`
 and `(z : C) → R`, returns an expression of type

src/Lean/Meta/Tactic/FunInd.lean

@@ -810,7 +810,8 @@ def cleanPackedArgs (eqnInfo : WF.EqnInfo) (value : Expr) : MetaM Expr := do
       let args := e.getAppArgs
       if eqnInfo.fixedPrefixSize + 1 ≤ args.size then
         let packedArg := args.back!
-          let (i, unpackedArgs) ← eqnInfo.argsPacker.unpack packedArg
+          let some (i, unpackedArgs) := eqnInfo.argsPacker.unpack packedArg
+            | throwError "Unexpected packedArg:{indentExpr packedArg}"
           let e' := .const eqnInfo.declNames[i]! e.getAppFn.constLevels!
           let e' := mkAppN e' args.pop
           let e' := mkAppN e' unpackedArgs
@@ -1110,11 +1111,16 @@ def isFunInductName (env : Environment) (name : Name) : Bool := Id.run do
   let .str p s := name | return false
   match s with
   | "induct" =>
-    if (WF.eqnInfoExt.find? env p).isSome then return true
+    if let some eqnInfo := WF.eqnInfoExt.find? env p then
+      unless eqnInfo.hasInduct do
+        return false
+      return true
     if (Structural.eqnInfoExt.find? env p).isSome then return true
     return false
   | "mutual_induct" =>
     if let some eqnInfo := WF.eqnInfoExt.find? env p then
+      unless eqnInfo.hasInduct do
+        return false
       if h : eqnInfo.declNames.size > 1 then
         return eqnInfo.declNames[0] = p
     if let some eqnInfo := Structural.eqnInfoExt.find? env p then

src/Lean/Parser/Basic.lean

@@ -804,18 +804,45 @@ where
       else
         normalState num c s
 
-def decimalNumberFn (startPos : String.Pos) (c : ParserContext) : ParserState → ParserState := fun s =>
-  let s     := takeWhileFn (fun c => c.isDigit) c s
+/--
+Parses a sequence of the form `many (many '_' >> many1 digit)`, but if `needDigit` is true the parsed result must be nonempty.
+
+Note: this does not report that it is expecting `_` if we reach EOI or an unexpected character.
+Rationale: this error happens if there is already a `_`, and while sequences of `_` are allowed, it's a bit perverse to suggest extending the sequence.
+-/
+partial def takeDigitsFn (isDigit : Char → Bool) (expecting : String) (needDigit : Bool) : ParserFn := fun c s =>
   let input := c.input
   let i     := s.pos
-  let curr  := input.get i
-  if curr == '.' || curr == 'e' || curr == 'E' then
+  if h : input.atEnd i then
+    if needDigit then
+      s.mkEOIError [expecting]
+    else
+      s
+  else
+    let curr := input.get' i h
+    if curr == '_' then takeDigitsFn isDigit expecting true c (s.next' c.input i h)
+    else if isDigit curr then takeDigitsFn isDigit expecting false c (s.next' c.input i h)
+    else if needDigit then s.mkUnexpectedError "unexpected character" (expected := [expecting])
+    else s
+
+def decimalNumberFn (startPos : String.Pos) (c : ParserContext) : ParserState → ParserState := fun s =>
+  let s     := takeDigitsFn (fun c => c.isDigit) "decimal number" false c s
+  let input := c.input
+  let i     := s.pos
+  if h : input.atEnd i then
+    mkNodeToken numLitKind startPos c s
+  else
+    let curr := input.get' i h
+    if curr == '.' || curr == 'e' || curr == 'E' then
+      parseScientific s
+    else
+      mkNodeToken numLitKind startPos c s
+where
+  parseScientific s :=
     let s := parseOptDot s
     let s := parseOptExp s
     mkNodeToken scientificLitKind startPos c s
-  else
-    mkNodeToken numLitKind startPos c s
-where
+
   parseOptDot s :=
     let input := c.input
     let i     := s.pos
@@ -824,7 +851,7 @@ where
       let i    := input.next i
       let curr := input.get i
       if curr.isDigit then
-        takeWhileFn (fun c => c.isDigit) c (s.setPos i)
+        takeDigitsFn (fun c => c.isDigit) "decimal number" false c (s.setPos i)
       else
         s.setPos i
     else
@@ -839,22 +866,22 @@ where
       let i    := if input.get i == '-' || input.get i == '+' then input.next i else i
       let curr := input.get i
       if curr.isDigit then
-        takeWhileFn (fun c => c.isDigit) c (s.setPos i)
+        takeDigitsFn (fun c => c.isDigit) "decimal number" false c (s.setPos i)
       else
         s.mkUnexpectedError "missing exponent digits in scientific literal"
     else
       s
 
 def binNumberFn (startPos : String.Pos) : ParserFn := fun c s =>
-  let s := takeWhile1Fn (fun c => c == '0' || c == '1') "binary number" c s
+  let s := takeDigitsFn (fun c => c == '0' || c == '1') "binary number" true c s
   mkNodeToken numLitKind startPos c s
 
 def octalNumberFn (startPos : String.Pos) : ParserFn := fun c s =>
-  let s := takeWhile1Fn (fun c => '0' ≤ c && c ≤ '7') "octal number" c s
+  let s := takeDigitsFn (fun c => '0' ≤ c && c ≤ '7') "octal number" true c s
   mkNodeToken numLitKind startPos c s
 
 def hexNumberFn (startPos : String.Pos) : ParserFn := fun c s =>
-  let s := takeWhile1Fn (fun c => ('0' ≤ c && c ≤ '9') || ('a' ≤ c && c ≤ 'f') || ('A' ≤ c && c ≤ 'F')) "hexadecimal number" c s
+  let s := takeDigitsFn (fun c => ('0' ≤ c && c ≤ '9') || ('a' ≤ c && c ≤ 'f') || ('A' ≤ c && c ≤ 'F')) "hexadecimal number" true c s
   mkNodeToken numLitKind startPos c s
 
 def numberFnAux : ParserFn := fun c s =>

src/Lean/ResolveName.lean

@@ -398,16 +398,22 @@ Aliases are considered first.
 
 When `fullNames` is true, returns either `n₀` or `_root_.n₀`.
 
+When `allowHorizAliases` is false, then "horizontal aliases" (ones that are not put into a parent namespace) are filtered out.
+The assumption is that non-horizontal aliases are "API exports" (i.e., intentional exports that should be considered to be the new canonical name).
+"Non-API exports" arise from (1) using `export` to add names to a namespace for dot notation or (2) projects that want names to be conveniently and permanently accessible in their own namespaces.
+
 This function is meant to be used for pretty printing.
 If `n₀` is an accessible name, then the result will be an accessible name.
 -/
-def unresolveNameGlobal [Monad m] [MonadResolveName m] [MonadEnv m] (n₀ : Name) (fullNames := false) : m Name := do
+def unresolveNameGlobal [Monad m] [MonadResolveName m] [MonadEnv m] (n₀ : Name) (fullNames := false) (allowHorizAliases := false) : m Name := do
   if n₀.hasMacroScopes then return n₀
   if fullNames then
     match (← resolveGlobalName n₀) with
       | [(potentialMatch, _)] => if (privateToUserName? potentialMatch).getD potentialMatch == n₀ then return n₀ else return rootNamespace ++ n₀
       | _ => return n₀ -- if can't resolve, return the original
   let mut initialNames := (getRevAliases (← getEnv) n₀).toArray
+  unless allowHorizAliases do
+    initialNames := initialNames.filter fun n => n.getPrefix.isPrefixOf n₀.getPrefix
   initialNames := initialNames.push (rootNamespace ++ n₀)
   for initialName in initialNames do
     if let some n ← unresolveNameCore initialName then

src/Std/Data/DHashMap/Internal/WF.lean

@@ -216,7 +216,7 @@ theorem expand.go_eq [BEq α] [Hashable α] [PartialEquivBEq α] (source : Array
     refine ih.trans ?_
     simp only [Array.get_eq_getElem, AssocList.foldl_eq, Array.toList_set]
     rw [List.drop_eq_getElem_cons hi, List.flatMap_cons, List.foldl_append,
-      List.drop_set_of_lt _ _ (by omega), Array.getElem_eq_getElem_toList]
+      List.drop_set_of_lt _ _ (by omega), Array.getElem_toList]
   · next i source target hi =>
     rw [expand.go_neg hi, List.drop_eq_nil_of_le, flatMap_nil, foldl_nil]
     rwa [Array.size_eq_length_toList, Nat.not_lt] at hi

src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean

@@ -77,12 +77,8 @@ theorem go_denote_eq (aig : AIG BVBit) (expr : BVExpr w) (assign : Assignment) :
     simp only [go, denote_blastAppend, RefVec.get_cast, Ref.cast_eq, eval_append,
       BitVec.getLsbD_append]
     split
-    · next hsplit =>
-      simp only [hsplit, decide_true, cond_true]
-      rw [rih]
-    · next hsplit =>
-      simp only [hsplit, decide_false, cond_false]
-      rw [go_denote_mem_prefix, lih]
+    · next hsplit => rw [rih]
+    · next hsplit => rw [go_denote_mem_prefix, lih]
   | replicate n expr ih => simp [go, ih, hidx]
   | signExtend v inner ih =>
     rename_i originalWidth
@@ -95,7 +91,7 @@ theorem go_denote_eq (aig : AIG BVBit) (expr : BVExpr w) (assign : Assignment) :
       rw [blastSignExtend_empty_eq_zeroExtend] at hgo
       · rw [← hgo]
         simp only [eval_signExtend]
-        rw [BitVec.signExtend_eq_not_setWidth_not_of_msb_false]
+        rw [BitVec.signExtend_eq_setWidth_of_msb_false]
         · simp only [denote_blastZeroExtend, ih, dite_eq_ite, Bool.if_false_right,
             BitVec.getLsbD_setWidth, hidx, decide_true, Bool.true_and, Bool.and_iff_right_iff_imp,
             decide_eq_true_eq]

src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Eq.lean

@@ -30,9 +30,9 @@ theorem mkEq_denote_eq (aig : AIG α) (pair : AIG.BinaryRefVec aig w) (assign :
   simp only [RefVec.denote_fold_and, RefVec.denote_zip, denote_mkBEqCached, beq_iff_eq]
   constructor
   · intro h
-    ext
+    ext i h'
     rw [← hleft, ← hright]
-    · simp [h]
+    · simp [h, h']
     · omega
     · omega
   · intro h idx hidx

src/Std/Tactic/BVDecide/LRAT/Internal/Clause.lean

@@ -297,7 +297,7 @@ theorem ofArray_eq (arr : Array (Literal (PosFin n)))
       dsimp; omega
     rw [List.getElem?_eq_getElem i_in_bounds, List.getElem?_eq_getElem i_in_bounds']
     simp only [List.get_eq_getElem, Nat.zero_add] at h
-    rw [← Array.getElem_eq_getElem_toList]
+    rw [Array.getElem_toList]
     simp [h]
   · have arr_data_length_le_i : arr.toList.length ≤ i := by
       dsimp; omega

src/Std/Tactic/BVDecide/LRAT/Internal/Formula/Lemmas.lean

@@ -497,7 +497,7 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
                 conv => rhs; rw [Array.size_mk]
                 exact hbound
               simp only [getElem!, id_eq_idx, Array.length_toList, idx_in_bounds2, ↓reduceDIte,
-                Fin.eta, Array.get_eq_getElem, Array.getElem_eq_getElem_toList, decidableGetElem?] at heq
+                Fin.eta, Array.get_eq_getElem, ← Array.getElem_toList, decidableGetElem?] at heq
               rw [hidx, hl] at heq
               simp only [unit, Option.some.injEq, DefaultClause.mk.injEq, List.cons.injEq, and_true] at heq
               simp only [← heq] at l_ne_b
@@ -530,7 +530,7 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
                 conv => rhs; rw [Array.size_mk]
                 exact hbound
               simp only [getElem!, id_eq_idx, Array.length_toList, idx_in_bounds2, ↓reduceDIte,
-                Fin.eta, Array.get_eq_getElem, Array.getElem_eq_getElem_toList, decidableGetElem?] at heq
+                Fin.eta, Array.get_eq_getElem, ← Array.getElem_toList, decidableGetElem?] at heq
               rw [hidx, hl] at heq
               simp only [unit, Option.some.injEq, DefaultClause.mk.injEq, List.cons.injEq, and_true] at heq
               have i_eq_l : i = l.1 := by rw [← heq]
@@ -590,7 +590,7 @@ theorem deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFor
                 conv => rhs; rw [Array.size_mk]
                 exact hbound
               simp only [getElem!, id_eq_idx, Array.length_toList, idx_in_bounds2, ↓reduceDIte,
-                Fin.eta, Array.get_eq_getElem, Array.getElem_eq_getElem_toList, decidableGetElem?] at heq
+                Fin.eta, Array.get_eq_getElem, ← Array.getElem_toList, decidableGetElem?] at heq
               rw [hidx] at heq
               simp only [Option.some.injEq] at heq
               rw [← heq] at hl

src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean

@@ -461,7 +461,7 @@ theorem existsRatHint_of_ratHintsExhaustive {n : Nat} (f : DefaultFormula n)
     constructor
     · rw [← Array.mem_toList]
       apply Array.getElem_mem_toList
-    · rw [← Array.getElem_eq_getElem_toList] at c'_in_f
+    · rw [Array.getElem_toList] at c'_in_f
       simp only [getElem!, Array.getElem_range, i_lt_f_clauses_size, dite_true,
         c'_in_f, DefaultClause.contains_iff, Array.get_eq_getElem, decidableGetElem?]
       simpa [Clause.toList] using negPivot_in_c'
@@ -472,8 +472,8 @@ theorem existsRatHint_of_ratHintsExhaustive {n : Nat} (f : DefaultFormula n)
     dsimp at *
     omega
   simp only [List.get_eq_getElem, Array.toList_map, Array.length_toList, List.getElem_map] at h'
-  rw [← Array.getElem_eq_getElem_toList] at h'
-  rw [← Array.getElem_eq_getElem_toList] at c'_in_f
+  rw [Array.getElem_toList] at h'
+  rw [Array.getElem_toList] at c'_in_f
   exists ⟨j.1, j_in_bounds⟩
   simp [getElem!, h', i_lt_f_clauses_size, dite_true, c'_in_f, decidableGetElem?]
 

src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean

@@ -1133,25 +1133,24 @@ theorem nodup_derivedLits {n : Nat} (f : DefaultFormula n)
       specialize h3 ⟨j.1, j_in_bounds⟩ j_ne_k
       simp only [derivedLits_arr_def, Fin.getElem_fin] at li_eq_lj
       simp only [Fin.getElem_fin, derivedLits_arr_def, ne_eq, li, li_eq_lj] at h3
-      simp only [List.get_eq_getElem, Array.getElem_eq_getElem_toList, not_true_eq_false] at h3
+      simp only [List.get_eq_getElem, ← Array.getElem_toList, not_true_eq_false] at h3
     · next k_ne_i =>
       have i_ne_k : ⟨i.1, i_in_bounds⟩ ≠ k := by intro i_eq_k; simp only [← i_eq_k, not_true] at k_ne_i
       specialize h3 ⟨i.1, i_in_bounds⟩ i_ne_k
-      simp +decide [Fin.getElem_fin, derivedLits_arr_def, ne_eq,
-        Array.getElem_eq_getElem_toList, li] at h3
+      simp +decide [Fin.getElem_fin, derivedLits_arr_def, ne_eq, li] at h3
   · by_cases li.2 = true
     · next li_eq_true =>
       have i_ne_k2 : ⟨i.1, i_in_bounds⟩ ≠ k2 := by
         intro i_eq_k2
         rw [← i_eq_k2] at k2_eq_false
         simp only [List.get_eq_getElem] at k2_eq_false
-        simp [derivedLits_arr_def, Array.getElem_eq_getElem_toList, k2_eq_false, li] at li_eq_true
+        simp [derivedLits_arr_def, k2_eq_false, li] at li_eq_true
       have j_ne_k2 : ⟨j.1, j_in_bounds⟩ ≠ k2 := by
         intro j_eq_k2
         rw [← j_eq_k2] at k2_eq_false
         simp only [List.get_eq_getElem] at k2_eq_false
-        simp only [derivedLits_arr_def, Fin.getElem_fin, Array.getElem_eq_getElem_toList] at li_eq_lj
-        simp [derivedLits_arr_def, Array.getElem_eq_getElem_toList, k2_eq_false, li_eq_lj, li] at li_eq_true
+        simp only [derivedLits_arr_def, Fin.getElem_fin] at li_eq_lj
+        simp [derivedLits_arr_def, k2_eq_false, li_eq_lj, li] at li_eq_true
       by_cases ⟨i.1, i_in_bounds⟩ = k1
       · next i_eq_k1 =>
         have j_ne_k1 : ⟨j.1, j_in_bounds⟩ ≠ k1 := by
@@ -1160,12 +1159,11 @@ theorem nodup_derivedLits {n : Nat} (f : DefaultFormula n)
           simp only [Fin.mk.injEq] at i_eq_k1
           exact i_ne_j (Fin.eq_of_val_eq i_eq_k1)
         specialize h3 ⟨j.1, j_in_bounds⟩ j_ne_k1 j_ne_k2
-        simp [li, li_eq_lj, derivedLits_arr_def, Array.getElem_eq_getElem_toList] at h3
+        simp [li, li_eq_lj, derivedLits_arr_def] at h3
       · next i_ne_k1 =>
         specialize h3 ⟨i.1, i_in_bounds⟩ i_ne_k1 i_ne_k2
         apply h3
-        simp +decide only [Fin.getElem_fin, Array.getElem_eq_getElem_toList,
-          ne_eq, derivedLits_arr_def, li]
+        simp +decide only [Fin.getElem_fin, ne_eq, derivedLits_arr_def, li]
         rfl
     · next li_eq_false =>
       simp only [Bool.not_eq_true] at li_eq_false
@@ -1173,13 +1171,13 @@ theorem nodup_derivedLits {n : Nat} (f : DefaultFormula n)
         intro i_eq_k1
         rw [← i_eq_k1] at k1_eq_true
         simp only [List.get_eq_getElem] at k1_eq_true
-        simp [derivedLits_arr_def, Array.getElem_eq_getElem_toList, k1_eq_true, li] at li_eq_false
+        simp [derivedLits_arr_def, k1_eq_true, li] at li_eq_false
       have j_ne_k1 : ⟨j.1, j_in_bounds⟩ ≠ k1 := by
         intro j_eq_k1
         rw [← j_eq_k1] at k1_eq_true
         simp only [List.get_eq_getElem] at k1_eq_true
-        simp only [derivedLits_arr_def, Fin.getElem_fin, Array.getElem_eq_getElem_toList] at li_eq_lj
-        simp [derivedLits_arr_def, Array.getElem_eq_getElem_toList, k1_eq_true, li_eq_lj, li] at li_eq_false
+        simp only [derivedLits_arr_def, Fin.getElem_fin] at li_eq_lj
+        simp [derivedLits_arr_def, k1_eq_true, li_eq_lj, li] at li_eq_false
       by_cases ⟨i.1, i_in_bounds⟩ = k2
       · next i_eq_k2 =>
         have j_ne_k2 : ⟨j.1, j_in_bounds⟩ ≠ k2 := by
@@ -1188,10 +1186,10 @@ theorem nodup_derivedLits {n : Nat} (f : DefaultFormula n)
           simp only [Fin.mk.injEq] at i_eq_k2
           exact i_ne_j (Fin.eq_of_val_eq i_eq_k2)
         specialize h3 ⟨j.1, j_in_bounds⟩ j_ne_k1 j_ne_k2
-        simp [li, li_eq_lj, derivedLits_arr_def, Array.getElem_eq_getElem_toList] at h3
+        simp [li, li_eq_lj, derivedLits_arr_def] at h3
       · next i_ne_k2 =>
         specialize h3 ⟨i.1, i_in_bounds⟩ i_ne_k1 i_ne_k2
-        simp +decide [Array.getElem_eq_getElem_toList, derivedLits_arr_def, li] at h3
+        simp +decide [derivedLits_arr_def, li] at h3
 
 theorem restoreAssignments_performRupCheck_base_case {n : Nat} (f : DefaultFormula n)
     (f_assignments_size : f.assignments.size = n)
@@ -1225,7 +1223,7 @@ theorem restoreAssignments_performRupCheck_base_case {n : Nat} (f : DefaultFormu
     constructor
     · apply Nat.zero_le
     · constructor
-      · simp only [derivedLits_arr_def, Fin.getElem_fin, Array.getElem_eq_getElem_toList, ← j_eq_i]
+      · simp only [derivedLits_arr_def, Fin.getElem_fin, ← j_eq_i]
         rfl
       · apply And.intro h1 ∘ And.intro h2
         intro k _ k_ne_j
@@ -1237,7 +1235,7 @@ theorem restoreAssignments_performRupCheck_base_case {n : Nat} (f : DefaultFormu
           apply Fin.ne_of_val_ne
           simp only
           exact Fin.val_ne_of_ne k_ne_j
-        simp only [Fin.getElem_fin, Array.getElem_eq_getElem_toList, ne_eq, derivedLits_arr_def]
+        simp only [Fin.getElem_fin, ne_eq, derivedLits_arr_def]
         exact h3 ⟨k.1, k_in_bounds⟩ k_ne_j
   · apply Or.inr ∘ Or.inr
     have j1_lt_derivedLits_arr_size : j1.1 < derivedLits_arr.size := by
@@ -1251,11 +1249,11 @@ theorem restoreAssignments_performRupCheck_base_case {n : Nat} (f : DefaultFormu
             ⟨j2.1, j2_lt_derivedLits_arr_size⟩,
             i_gt_zero, Nat.zero_le j1.1, Nat.zero_le j2.1, ?_⟩
     constructor
-    · simp only [derivedLits_arr_def, Fin.getElem_fin, Array.getElem_eq_getElem_toList, ← j1_eq_i]
+    · simp only [derivedLits_arr_def, Fin.getElem_fin, ← j1_eq_i]
       rw [← j1_eq_true]
       rfl
     · constructor
-      · simp only [derivedLits_arr_def, Fin.getElem_fin, Array.getElem_eq_getElem_toList, ← j2_eq_i]
+      · simp only [derivedLits_arr_def, Fin.getElem_fin, ← j2_eq_i]
         rw [← j2_eq_false]
         rfl
       · apply And.intro h1 ∘ And.intro h2
@@ -1272,7 +1270,7 @@ theorem restoreAssignments_performRupCheck_base_case {n : Nat} (f : DefaultFormu
           apply Fin.ne_of_val_ne
           simp only
           exact Fin.val_ne_of_ne k_ne_j2
-        simp only [Fin.getElem_fin, Array.getElem_eq_getElem_toList, ne_eq, derivedLits_arr_def]
+        simp only [Fin.getElem_fin, ne_eq, derivedLits_arr_def]
         exact h3 ⟨k.1, k_in_bounds⟩ k_ne_j1 k_ne_j2
 
 theorem restoreAssignments_performRupCheck {n : Nat} (f : DefaultFormula n) (f_assignments_size : f.assignments.size = n)

src/Std/Tactic/BVDecide/Normalize/BitVec.lean

@@ -168,13 +168,13 @@ attribute [bv_normalize] BitVec.and_self
 
 @[bv_normalize]
 theorem BitVec.and_contra (a : BitVec w) : a &&& ~~~a = 0#w := by
-  ext
-  simp
+  ext i h
+  simp [h]
 
 @[bv_normalize]
 theorem BitVec.and_contra' (a : BitVec w) : ~~~a &&& a = 0#w := by
-  ext
-  simp
+  ext i h
+  simp [h]
 
 @[bv_normalize]
 theorem BitVec.add_not (a : BitVec w) : a + ~~~a = (-1#w) := by

src/include/lean/lean.h

@@ -614,6 +614,11 @@ static inline double lean_ctor_get_float(b_lean_obj_arg o, unsigned offset) {
     return *((double*)((uint8_t*)(lean_ctor_obj_cptr(o)) + offset));
 }
 
+static inline float lean_ctor_get_float32(b_lean_obj_arg o, unsigned offset) {
+    assert(offset >= lean_ctor_num_objs(o) * sizeof(void*));
+    return *((float*)((uint8_t*)(lean_ctor_obj_cptr(o)) + offset));
+}
+
 static inline void lean_ctor_set_usize(b_lean_obj_arg o, unsigned i, size_t v) {
     assert(i >= lean_ctor_num_objs(o));
     *((size_t*)(lean_ctor_obj_cptr(o) + i)) = v;
@@ -644,6 +649,11 @@ static inline void lean_ctor_set_float(b_lean_obj_arg o, unsigned offset, double
     *((double*)((uint8_t*)(lean_ctor_obj_cptr(o)) + offset)) = v;
 }
 
+static inline void lean_ctor_set_float32(b_lean_obj_arg o, unsigned offset, float v) {
+    assert(offset >= lean_ctor_num_objs(o) * sizeof(void*));
+    *((float*)((uint8_t*)(lean_ctor_obj_cptr(o)) + offset)) = v;
+}
+
 /* Closures */
 
 static inline void * lean_closure_fun(lean_object * o) { return lean_to_closure(o)->m_fun; }
@@ -2561,6 +2571,15 @@ LEAN_EXPORT uint8_t lean_float_isfinite(double a);
 LEAN_EXPORT uint8_t lean_float_isinf(double a);
 LEAN_EXPORT lean_obj_res lean_float_frexp(double a);
 
+/* Float32 */
+
+LEAN_EXPORT lean_obj_res lean_float32_to_string(float a);
+LEAN_EXPORT float lean_float32_scaleb(float a, b_lean_obj_arg b);
+LEAN_EXPORT uint8_t lean_float32_isnan(float a);
+LEAN_EXPORT uint8_t lean_float32_isfinite(float a);
+LEAN_EXPORT uint8_t lean_float32_isinf(float a);
+LEAN_EXPORT lean_obj_res lean_float32_frexp(float a);
+
 /* Boxing primitives */
 
 static inline lean_obj_res lean_box_uint32(uint32_t v) {
@@ -2615,6 +2634,16 @@ static inline double lean_unbox_float(b_lean_obj_arg o) {
     return lean_ctor_get_float(o, 0);
 }
 
+static inline lean_obj_res lean_box_float32(float v) {
+    lean_obj_res r = lean_alloc_ctor(0, 0, sizeof(float)); // NOLINT
+    lean_ctor_set_float32(r, 0, v);
+    return r;
+}
+
+static inline float lean_unbox_float32(b_lean_obj_arg o) {
+    return lean_ctor_get_float32(o, 0);
+}
+
 /* Debugging helper functions */
 
 LEAN_EXPORT lean_object * lean_dbg_trace(lean_obj_arg s, lean_obj_arg fn);
@@ -2729,6 +2758,40 @@ static inline uint8_t lean_float_decLe(double a, double b) { return a <= b; }
 static inline uint8_t lean_float_decLt(double a, double b) { return a < b; }
 static inline double lean_uint64_to_float(uint64_t a) { return (double) a; }
 
+/* float32 primitives */
+static inline uint8_t lean_float32_to_uint8(float a) {
+    return 0. <= a ? (a < 256. ? (uint8_t)a : UINT8_MAX) : 0;
+}
+static inline uint16_t lean_float32_to_uint16(float a) {
+    return 0. <= a ? (a < 65536. ? (uint16_t)a : UINT16_MAX) : 0;
+}
+static inline uint32_t lean_float32_to_uint32(float a) {
+    return 0. <= a ? (a < 4294967296. ? (uint32_t)a : UINT32_MAX) : 0;
+}
+static inline uint64_t lean_float32_to_uint64(float a) {
+    return 0. <= a ? (a < 18446744073709551616. ? (uint64_t)a : UINT64_MAX) : 0;
+}
+static inline size_t lean_float32_to_usize(float a) {
+    if (sizeof(size_t) == sizeof(uint64_t)) // NOLINT
+        return (size_t) lean_float32_to_uint64(a); // NOLINT
+    else
+        return (size_t) lean_float32_to_uint32(a); // NOLINT
+}
+LEAN_EXPORT float lean_float32_of_bits(uint32_t u);
+LEAN_EXPORT uint32_t lean_float32_to_bits(float d);
+static inline float lean_float32_add(float a, float b) { return a + b; }
+static inline float lean_float32_sub(float a, float b) { return a - b; }
+static inline float lean_float32_mul(float a, float b) { return a * b; }
+static inline float lean_float32_div(float a, float b) { return a / b; }
+static inline float lean_float32_negate(float a) { return -a; }
+static inline uint8_t lean_float32_beq(float a, float b) { return a == b; }
+static inline uint8_t lean_float32_decLe(float a, float b) { return a <= b; }
+static inline uint8_t lean_float32_decLt(float a, float b) { return a < b; }
+static inline float lean_uint64_to_float32(uint64_t a) { return (float) a; }
+
+static inline float lean_float_to_float32(double a) { return (float)a; }
+static inline double lean_float32_to_float(float a) { return (double)a; }
+
 /* Efficient C implementations of defns used by the compiler */
 static inline size_t lean_hashmap_mk_idx(lean_obj_arg sz, uint64_t hash) {
     return (size_t)(hash & (lean_unbox(sz) - 1));

src/library/compiler/ir.cpp

@@ -123,6 +123,8 @@ static ir::type to_ir_type(expr const & e) {
             return ir::type::USize;
         } else if (const_name(e) == get_float_name()) {
             return ir::type::Float;
+        } else if (const_name(e) == get_float32_name()) {
+            return ir::type::Float32;
         }
      } else if (is_pi(e)) {
         return ir::type::Object;
@@ -350,6 +352,16 @@ class to_ir_fn {
         return ir::mk_sset(to_var_id(args[0]), n, offset, to_var_id(args[1]), ir::type::Float, b);
     }
 
+    ir::fn_body visit_f32set(local_decl const & decl, ir::fn_body const & b) {
+        expr val = *decl.get_value();
+        buffer<expr> args;
+        expr const & fn = get_app_args(val, args);
+        lean_assert(args.size() == 2);
+        unsigned n, offset;
+        lean_verify(is_llnf_f32set(fn, n, offset));
+        return ir::mk_sset(to_var_id(args[0]), n, offset, to_var_id(args[1]), ir::type::Float32, b);
+    }
+
     ir::fn_body visit_uset(local_decl const & decl, ir::fn_body const & b) {
         expr val = *decl.get_value();
         buffer<expr> args;
@@ -417,6 +429,8 @@ class to_ir_fn {
                 return visit_sset(decl, b);
             else if (is_llnf_fset(fn))
                 return visit_fset(decl, b);
+            else if (is_llnf_f32set(fn))
+                return visit_f32set(decl, b);
             else if (is_llnf_uset(fn))
                 return visit_uset(decl, b);
             else if (is_llnf_proj(fn))
@@ -449,7 +463,7 @@ class to_ir_fn {
                 expr new_fvar   = m_lctx.mk_local_decl(ngen(), n, type, val);
                 fvars.push_back(new_fvar);
                 expr const & op = get_app_fn(val);
-                if (is_llnf_sset(op) || is_llnf_fset(op) || is_llnf_uset(op)) {
+                if (is_llnf_sset(op) || is_llnf_fset(op) || is_llnf_f32set(op) || is_llnf_uset(op)) {
                     /* In the Lean IR, sset and uset are instructions that perform destructive updates. */
                     subst.push_back(app_arg(app_fn(val)));
                 } else {

src/library/compiler/ir.h

@@ -14,12 +14,13 @@ namespace ir {
 inductive IRType
 | float | uint8 | uint16 | uint32 | uint64 | usize
 | irrelevant | object | tobject
+| float32
 | struct (leanTypeName : Option Name) (types : Array IRType) : IRType
 | union (leanTypeName : Name) (types : Array IRType) : IRType
 
 Remark: we don't create struct/union types from C++.
 */
-enum class type { Float, UInt8, UInt16, UInt32, UInt64, USize, Irrelevant, Object, TObject };
+enum class type { Float, UInt8, UInt16, UInt32, UInt64, USize, Irrelevant, Object, TObject, Float32, Struct, Union };
 
 typedef nat        var_id;
 typedef nat        jp_id;

src/library/compiler/ir_interpreter.cpp

@@ -188,6 +188,11 @@ option_ref<decl> find_ir_decl(environment const & env, name const & n) {
 
 extern "C" double lean_float_of_nat(lean_obj_arg a);
 
+// TODO: define in Lean like `lean_float_of_nat`
+float lean_float32_of_nat(lean_obj_arg a) {
+    return lean_float_of_nat(a);
+}
+
 static string_ref * g_mangle_prefix = nullptr;
 static string_ref * g_boxed_suffix = nullptr;
 static string_ref * g_boxed_mangled_suffix = nullptr;
@@ -227,6 +232,7 @@ union value {
     uint64   m_num; // big enough for any unboxed integral type
     static_assert(sizeof(size_t) <= sizeof(uint64), "uint64 should be the largest unboxed type"); // NOLINT
     double   m_float;
+    float    m_float32;
     object * m_obj;
 
     value() {}
@@ -240,36 +246,50 @@ union value {
         v.m_float = f;
         return v;
     }
+
+    static value from_float32(float f) {
+        value v;
+        v.m_float32 = f;
+        return v;
+    }
 };
 
 object * box_t(value v, type t) {
     switch (t) {
-        case type::Float: return box_float(v.m_float);
-        case type::UInt8: return box(v.m_num);
-        case type::UInt16: return box(v.m_num);
-        case type::UInt32: return box_uint32(v.m_num);
-        case type::UInt64: return box_uint64(v.m_num);
-        case type::USize: return box_size_t(v.m_num);
-        case type::Object:
-        case type::TObject:
-        case type::Irrelevant:
-            return v.m_obj;
+    case type::Float:   return box_float(v.m_float);
+    case type::Float32: return box_float(v.m_float32);
+    case type::UInt8:   return box(v.m_num);
+    case type::UInt16:  return box(v.m_num);
+    case type::UInt32:  return box_uint32(v.m_num);
+    case type::UInt64:  return box_uint64(v.m_num);
+    case type::USize:   return box_size_t(v.m_num);
+    case type::Object:
+    case type::TObject:
+    case type::Irrelevant:
+        return v.m_obj;
+    case type::Struct:
+    case type::Union:
+        throw exception("not implemented yet");
     }
     lean_unreachable();
 }
 
 value unbox_t(object * o, type t) {
     switch (t) {
-        case type::Float: return value::from_float(unbox_float(o));
-        case type::UInt8: return unbox(o);
-        case type::UInt16: return unbox(o);
-        case type::UInt32: return unbox_uint32(o);
-        case type::UInt64: return unbox_uint64(o);
-        case type::USize: return unbox_size_t(o);
-        case type::Irrelevant:
-        case type::Object:
-        case type::TObject:
-            break;
+    case type::Float:   return value::from_float(unbox_float(o));
+    case type::Float32: return value::from_float32(unbox_float32(o));
+    case type::UInt8:   return unbox(o);
+    case type::UInt16:  return unbox(o);
+    case type::UInt32:  return unbox_uint32(o);
+    case type::UInt64:  return unbox_uint64(o);
+    case type::USize:   return unbox_size_t(o);
+    case type::Irrelevant:
+    case type::Object:
+    case type::TObject:
+        break;
+    case type::Struct:
+    case type::Union:
+        throw exception("not implemented yet");
     }
     lean_unreachable();
 }
@@ -278,6 +298,8 @@ value unbox_t(object * o, type t) {
 void print_value(tout & ios, value const & v, type t) {
     if (t == type::Float) {
         ios << v.m_float;
+    } else if (t == type::Float32) {
+        ios << v.m_float32;
     } else if (type_is_scalar(t)) {
         ios << v.m_num;
     } else {
@@ -472,6 +494,7 @@ private:
                 object * o = var(expr_sproj_obj(e)).m_obj;
                 switch (t) {
                     case type::Float: return value::from_float(cnstr_get_float(o, offset));
+                    case type::Float32: return value::from_float32(cnstr_get_float32(o, offset));
                     case type::UInt8: return cnstr_get_uint8(o, offset);
                     case type::UInt16: return cnstr_get_uint16(o, offset);
                     case type::UInt32: return cnstr_get_uint32(o, offset);
@@ -480,6 +503,8 @@ private:
                     case type::Irrelevant:
                     case type::Object:
                     case type::TObject:
+                    case type::Struct:
+                    case type::Union:
                         break;
                 }
                 throw exception("invalid instruction");
@@ -530,6 +555,9 @@ private:
                             case type::Float:
                                 lean_inc(n.raw());
                                 return value::from_float(lean_float_of_nat(n.raw()));
+                            case type::Float32:
+                                lean_inc(n.raw());
+                                return value::from_float32(lean_float32_of_nat(n.raw()));
                             case type::UInt8:
                             case type::UInt16:
                             case type::UInt32:
@@ -543,6 +571,9 @@ private:
                                 return n.to_obj_arg();
                             case type::Irrelevant:
                                 break;
+                            case type::Union:
+                            case type::Struct:
+                                break;
                         }
                         throw exception("invalid instruction");
                     }
@@ -654,6 +685,7 @@ private:
                     lean_assert(is_exclusive(o));
                     switch (fn_body_sset_type(b)) {
                         case type::Float: cnstr_set_float(o, offset, v.m_float); break;
+                        case type::Float32: cnstr_set_float32(o, offset, v.m_float32); break;
                         case type::UInt8: cnstr_set_uint8(o, offset, v.m_num); break;
                         case type::UInt16: cnstr_set_uint16(o, offset, v.m_num); break;
                         case type::UInt32: cnstr_set_uint32(o, offset, v.m_num); break;
@@ -662,6 +694,8 @@ private:
                         case type::Irrelevant:
                         case type::Object:
                         case type::TObject:
+                        case type::Struct:
+                        case type::Union:
                             throw exception(sstream() << "invalid instruction");
                     }
                     b = fn_body_sset_cont(b);
@@ -807,6 +841,7 @@ private:
             // constants do not have boxed wrappers, but we'll survive
             switch (t) {
                 case type::Float: return value::from_float(*static_cast<double *>(e.m_addr));
+                case type::Float32: return value::from_float32(*static_cast<float *>(e.m_addr));
                 case type::UInt8: return *static_cast<uint8 *>(e.m_addr);
                 case type::UInt16: return *static_cast<uint16 *>(e.m_addr);
                 case type::UInt32: return *static_cast<uint32 *>(e.m_addr);
@@ -816,6 +851,9 @@ private:
                 case type::TObject:
                 case type::Irrelevant:
                     return *static_cast<object **>(e.m_addr);
+                case type::Struct:
+                case type::Union:
+                    throw exception("not implemented yet");
             }
         }
 

src/library/compiler/llnf.cpp

@@ -34,6 +34,7 @@ static char const * g_cnstr = "_cnstr";
 static name * g_reuse       = nullptr;
 static name * g_reset       = nullptr;
 static name * g_fset        = nullptr;
+static name * g_f32set      = nullptr;
 static name * g_sset        = nullptr;
 static name * g_uset        = nullptr;
 static name * g_proj        = nullptr;
@@ -162,6 +163,9 @@ bool is_llnf_sset(expr const & e, unsigned & sz, unsigned & n, unsigned & offset
 expr mk_llnf_fset(unsigned n, unsigned offset) { return mk_constant(name(name(*g_fset, n), offset)); }
 bool is_llnf_fset(expr const & e, unsigned & n, unsigned & offset) { return is_llnf_binary_primitive(e, *g_fset, n, offset); }
 
+expr mk_llnf_f32set(unsigned n, unsigned offset) { return mk_constant(name(name(*g_f32set, n), offset)); }
+bool is_llnf_f32set(expr const & e, unsigned & n, unsigned & offset) { return is_llnf_binary_primitive(e, *g_f32set, n, offset); }
+
 /* The `_uset.<n>` instruction sets a `usize` value in a constructor object at offset `sizeof(void*)*n`. */
 expr mk_llnf_uset(unsigned n) { return mk_constant(name(*g_uset, n)); }
 bool is_llnf_uset(expr const & e, unsigned & n) { return is_llnf_unary_primitive(e, *g_uset, n); }
@@ -218,6 +222,7 @@ bool is_llnf_op(expr const & e) {
         is_llnf_reset(e)   ||
         is_llnf_sset(e)    ||
         is_llnf_fset(e)    ||
+        is_llnf_f32set(e)  ||
         is_llnf_uset(e)    ||
         is_llnf_proj(e)    ||
         is_llnf_sproj(e)   ||
@@ -520,6 +525,10 @@ class to_lambda_pure_fn {
         return mk_app(mk_llnf_fset(num, offset), major, v);
     }
 
+    expr mk_f32set(expr const & major, unsigned num, unsigned offset, expr const & v) {
+        return mk_app(mk_llnf_f32set(num, offset), major, v);
+    }
+
     expr mk_uset(expr const & major, unsigned idx, expr const & v) {
         return mk_app(mk_llnf_uset(idx), major, v);
     }
@@ -586,7 +595,7 @@ class to_lambda_pure_fn {
                         fields.push_back(mk_let_decl(info.get_type(), mk_uproj(major, info.m_idx)));
                         break;
                     case field_info::Scalar:
-                        if (info.is_float()) {
+                        if (info.is_float() || info.is_float32()) {
                             fields.push_back(mk_let_decl(info.get_type(), mk_fproj(major, info.m_idx, info.m_offset)));
                         } else {
                             fields.push_back(mk_let_decl(info.get_type(), mk_sproj(major, info.m_size, info.m_idx, info.m_offset)));
@@ -686,6 +695,8 @@ class to_lambda_pure_fn {
                 }
                 if (info.is_float()) {
                     r = mk_let_decl(mk_enf_object_type(), mk_fset(r, info.m_idx, info.m_offset, args[j]));
+                } else if (info.is_float32()) {
+                    r = mk_let_decl(mk_enf_object_type(), mk_f32set(r, info.m_idx, info.m_offset, args[j]));
                 } else {
                     r = mk_let_decl(mk_enf_object_type(), mk_sset(r, info.m_size, info.m_idx, info.m_offset, args[j]));
                 }
@@ -731,7 +742,7 @@ class to_lambda_pure_fn {
                 break;
             case field_info::Scalar:
                 if (proj_idx(e) == i) {
-                    if (info.is_float()) {
+                    if (info.is_float() || info.is_float32()) {
                         return mk_fproj(visit(proj_expr(e)), info.m_idx, info.m_offset);
                     } else {
                         return mk_sproj(visit(proj_expr(e)), info.m_size, info.m_idx, info.m_offset);
@@ -834,6 +845,8 @@ void initialize_llnf() {
     mark_persistent(g_sset->raw());
     g_fset      = new name("_fset");
     mark_persistent(g_fset->raw());
+    g_f32set      = new name("_f32set");
+    mark_persistent(g_f32set->raw());
     g_uset      = new name("_uset");
     mark_persistent(g_uset->raw());
     g_proj      = new name("_proj");
@@ -864,6 +877,7 @@ void finalize_llnf() {
     delete g_reset;
     delete g_sset;
     delete g_fset;
+    delete g_f32set;
     delete g_proj;
     delete g_sproj;
     delete g_fproj;

src/library/compiler/llnf.h

@@ -26,6 +26,7 @@ bool is_llnf_fproj(expr const & e, unsigned & n, unsigned & offset);
 bool is_llnf_uproj(expr const & e, unsigned & idx);
 bool is_llnf_sset(expr const & e, unsigned & sz, unsigned & n, unsigned & offset);
 bool is_llnf_fset(expr const & e, unsigned & n, unsigned & offset);
+bool is_llnf_f32set(expr const & e, unsigned & n, unsigned & offset);
 bool is_llnf_uset(expr const & e, unsigned & n);
 bool is_llnf_jmp(expr const & e);
 bool is_llnf_unbox(expr const & e, unsigned & n);
@@ -43,6 +44,7 @@ inline bool is_llnf_fproj(expr const & e) { unsigned d1, d2; return is_llnf_fpro
 inline bool is_llnf_uproj(expr const & e) { unsigned d; return is_llnf_uproj(e, d); }
 inline bool is_llnf_sset(expr const & e) { unsigned d1, d2, d3; return is_llnf_sset(e, d1, d2, d3); }
 inline bool is_llnf_fset(expr const & e) { unsigned d1, d2; return is_llnf_fset(e, d1, d2); }
+inline bool is_llnf_f32set(expr const & e) { unsigned d1, d2; return is_llnf_f32set(e, d1, d2); }
 inline bool is_llnf_uset(expr const & e) { unsigned d; return is_llnf_uset(e, d); }
 inline bool is_llnf_box(expr const & e) { unsigned n; return is_llnf_box(e, n); }
 inline bool is_llnf_unbox(expr const & e) { unsigned n; return is_llnf_unbox(e, n); }
@@ -66,6 +68,7 @@ struct field_info {
         m_kind(Scalar), m_size(sz), m_idx(num), m_offset(offset), m_type(type) {}
     expr get_type() const { return m_type; }
     bool is_float() const { return is_constant(m_type, get_float_name()); }
+    bool is_float32() const { return is_constant(m_type, get_float32_name()); }
     static field_info mk_irrelevant() { return field_info(); }
     static field_info mk_object(unsigned idx) { return field_info(idx); }
     static field_info mk_usize() { return field_info(0, true); }

src/library/compiler/util.cpp

@@ -386,6 +386,7 @@ bool is_runtime_builtin_type(name const & n) {
         n == get_uint64_name() ||
         n == get_usize_name()  ||
         n == get_float_name()  ||
+        n == get_float32_name() ||
         n == get_thunk_name()  ||
         n == get_task_name()   ||
         n == get_array_name()  ||
@@ -403,7 +404,8 @@ bool is_runtime_scalar_type(name const & n) {
         n == get_uint32_name() ||
         n == get_uint64_name() ||
         n == get_usize_name()  ||
-        n == get_float_name();
+        n == get_float_name()  ||
+        n == get_float32_name();
 }
 
 bool is_llnf_unboxed_type(expr const & type) {
@@ -493,6 +495,8 @@ expr mk_runtime_type(type_checker::state & st, local_ctx const & lctx, expr e) {
                 return e;
             } else if (c == get_float_name()) {
                 return e;
+            } else if (c == get_float32_name()) {
+                return e;
             } else if (optional<unsigned> nbytes = is_enum_type(st.env(), c)) {
                 return *to_uint_type(*nbytes);
             }
@@ -807,6 +811,7 @@ void initialize_compiler_util() {
     g_builtin_scalar_size->emplace_back(get_uint32_name(), 4);
     g_builtin_scalar_size->emplace_back(get_uint64_name(), 8);
     g_builtin_scalar_size->emplace_back(get_float_name(),  8);
+    g_builtin_scalar_size->emplace_back(get_float32_name(), 4);
 }
 
 void finalize_compiler_util() {

src/library/constants.cpp

@@ -44,6 +44,7 @@ name const * g_eq_subst = nullptr;
 name const * g_eq_symm = nullptr;
 name const * g_eq_trans = nullptr;
 name const * g_float = nullptr;
+name const * g_float32 = nullptr;
 name const * g_float_array = nullptr;
 name const * g_float_array_data = nullptr;
 name const * g_false = nullptr;
@@ -191,6 +192,8 @@ void initialize_constants() {
     mark_persistent(g_eq_trans->raw());
     g_float = new name{"Float"};
     mark_persistent(g_float->raw());
+    g_float32 = new name{"Float32"};
+    mark_persistent(g_float32->raw());
     g_float_array = new name{"FloatArray"};
     mark_persistent(g_float_array->raw());
     g_float_array_data = new name{"FloatArray", "data"};
@@ -362,6 +365,7 @@ void finalize_constants() {
     delete g_eq_symm;
     delete g_eq_trans;
     delete g_float;
+    delete g_float32;
     delete g_float_array;
     delete g_float_array_data;
     delete g_false;
@@ -468,6 +472,7 @@ name const & get_eq_subst_name() { return *g_eq_subst; }
 name const & get_eq_symm_name() { return *g_eq_symm; }
 name const & get_eq_trans_name() { return *g_eq_trans; }
 name const & get_float_name() { return *g_float; }
+name const & get_float32_name() { return *g_float32; }
 name const & get_float_array_name() { return *g_float_array; }
 name const & get_float_array_data_name() { return *g_float_array_data; }
 name const & get_false_name() { return *g_false; }

src/library/constants.h

@@ -46,6 +46,7 @@ name const & get_eq_subst_name();
 name const & get_eq_symm_name();
 name const & get_eq_trans_name();
 name const & get_float_name();
+name const & get_float32_name();
 name const & get_float_array_name();
 name const & get_float_array_data_name();
 name const & get_false_name();

src/library/constants.txt

@@ -39,6 +39,7 @@ Eq.subst
 Eq.symm
 Eq.trans
 Float
+Float32
 FloatArray
 FloatArray.data
 False

src/runtime/object.cpp

@@ -1661,6 +1661,58 @@ extern "C" LEAN_EXPORT uint64_t lean_float_to_bits(double d)
     return ret;
 }
 
+// =======================================
+// Float32
+
+extern "C" LEAN_EXPORT lean_obj_res lean_float32_to_string(float a) {
+    if (isnan(a))
+        // override NaN because we don't want NaNs to be distinguishable
+        // because the sign bit / payload bits can be architecture-dependent
+        return mk_ascii_string_unchecked("NaN");
+    else
+        return mk_ascii_string_unchecked(std::to_string(a));
+}
+
+extern "C" LEAN_EXPORT float lean_float32_scaleb(float a, b_lean_obj_arg b) {
+   if (lean_is_scalar(b)) {
+     return scalbn(a, lean_scalar_to_int(b));
+   } else if (a == 0 || mpz_value(b).is_neg()) {
+     return 0;
+   } else {
+     return a * (1.0 / 0.0);
+   }
+}
+
+extern "C" LEAN_EXPORT uint8_t lean_float32_isnan(float a) { return (bool) isnan(a); }
+extern "C" LEAN_EXPORT uint8_t lean_float32_isfinite(float a) { return (bool) isfinite(a); }
+extern "C" LEAN_EXPORT uint8_t lean_float32_isinf(float a) { return (bool) isinf(a); }
+extern "C" LEAN_EXPORT obj_res lean_float32_frexp(float a) {
+    object* r = lean_alloc_ctor(0, 2, 0);
+    int exp;
+    lean_ctor_set(r, 0, lean_box_float32(frexp(a, &exp)));
+    lean_ctor_set(r, 1, isfinite(a) ? lean_int_to_int(exp) : lean_box(0));
+    return r;
+}
+
+extern "C" LEAN_EXPORT float lean_float32_of_bits(uint32_t u)
+{
+    static_assert(sizeof(float) == sizeof(u), "`float` unexpected size.");
+    float ret;
+    std::memcpy(&ret, &u, sizeof(float));
+    if (isnan(ret))
+        ret = std::numeric_limits<float>::quiet_NaN();
+    return ret;
+}
+
+extern "C" LEAN_EXPORT uint32_t lean_float32_to_bits(float d)
+{
+    uint32_t ret;
+    if (isnan(d))
+        d = std::numeric_limits<float>::quiet_NaN();
+    std::memcpy(&ret, &d, sizeof(float));
+    return ret;
+}
+
 // =======================================
 // Strings
 

src/runtime/object.h

@@ -85,11 +85,13 @@ inline uint16 cnstr_get_uint16(b_obj_arg o, unsigned offset) { return lean_ctor_
 inline uint32 cnstr_get_uint32(b_obj_arg o, unsigned offset) { return lean_ctor_get_uint32(o, offset); }
 inline uint64 cnstr_get_uint64(b_obj_arg o, unsigned offset) { return lean_ctor_get_uint64(o, offset); }
 inline double cnstr_get_float(b_obj_arg o, unsigned offset) { return lean_ctor_get_float(o, offset); }
+inline float cnstr_get_float32(b_obj_arg o, unsigned offset) { return lean_ctor_get_float32(o, offset); }
 inline void cnstr_set_uint8(b_obj_arg o, unsigned offset, uint8 v) { lean_ctor_set_uint8(o, offset, v); }
 inline void cnstr_set_uint16(b_obj_arg o, unsigned offset, uint16 v) { lean_ctor_set_uint16(o, offset, v); }
 inline void cnstr_set_uint32(b_obj_arg o, unsigned offset, uint32 v) { lean_ctor_set_uint32(o, offset, v); }
 inline void cnstr_set_uint64(b_obj_arg o, unsigned offset, uint64 v) { lean_ctor_set_uint64(o, offset, v); }
 inline void cnstr_set_float(b_obj_arg o, unsigned offset, double v) { lean_ctor_set_float(o, offset, v); }
+inline void cnstr_set_float32(b_obj_arg o, unsigned offset, float v) { lean_ctor_set_float32(o, offset, v); }
 
 // =======================================
 // Closures
@@ -372,6 +374,7 @@ inline obj_res box_uint64(unsigned long long v) { return lean_box_uint64(v); }
 inline unsigned long long unbox_uint64(b_obj_arg o) { return lean_unbox_uint64(o); }
 inline obj_res box_float(double v) { return lean_box_float(v); }
 inline double unbox_float(b_obj_arg o) { return lean_unbox_float(o); }
+inline float unbox_float32(b_obj_arg o) { return lean_unbox_float32(o); }
 inline obj_res box_size_t(size_t v) { return lean_box_usize(v); }
 inline size_t unbox_size_t(b_obj_arg o) { return lean_unbox_usize(o); }