This PR moves the validation of cross-package `import all` to Lake and
the syntax validation of import keywords (`public`, `meta`, and `all`)
to the two import parsers.
It also fixes the error reporting of the fast import parser
(`Lean.parseImports`) and adds positions to its errors.
This PR addresses an outstanding feature in the module system to
automatically mark `let rec` and `where` helper declarations as private
unless they are defined in a public context such as under `@[expose]`.
This PR removes an error which implicitly assumes that the sort of type
dependency between erased types present in the test being added can not
occur. It would be difficult to refine the error using only the
information present in LCNF types, and it is of very little ongoing
value (I don't recall it ever finding an actual problem), so it makes
more sense to delete it.
Fixes#9692.
This PR changes the LCNF `elimDeadBranches` pass so that it considers
all non-`Nat` literal types to be `⊤`. It turns out that fixing this to
correctly handle all of these types with the current abstract value
representation is surprisingly nontrivial, and it's better to just land
the fix first.
This PR adds a version of `CommRing.Expr.toPoly` optimized for kernel
reduction. We use this function not only to implement `grind ring`, but
also to interface the ring module with `grind cutsat`.
This PR updates `release_repos.yml` to reflect that `import-graph` no
longer depends on `batteries`, and reorders the repositories to better
reflect dependencies.
This PR adds propagation rules for functions that take singleton types.
This feature is useful for discharging verification conditions produced
by `mvcgen`. For example:
```lean
example (h : (fun (_ : Unit) => x + 1) = (fun _ => 1 + y)) : x = y := by
grind
```
This removes the early call to `contradiction` from `simpH`, and
replaces it with a quick check if the pattern start with different
constructors.
We already call `simpH` quadratically often (unavoidable), so we want it
to be quick. Most common contradictions are found later on, so maybe we
don't want to the expensive `contradiction` tactic to be run early.
May help with #9598.
This PR adjusts the formatting type classes for `lake query` to no
longer require both a text and JSON form and instead work with any
combination of the two. The classes have also been renamed. In addition,
the query formatting of a text module header has been improved to only
produce valid headers.
This PR restricts Lake's production of thin archives to only the Windows
core build (i.e., `bootstrap = true`). The unbundled `ar` usually used
for core builds on macOS does not support `--thin`, so we avoid using it
unless necessary.
