This PR makes the new compiler's specialization pass compute closures
the same way as the old compiler, in particular when it comes to
variables captured by lambdas.
This PR makes it possible for `bv_decide` to tackle situations for its
enum type preprocessing where the enums themselves are use in a
dependently type context (for example inside of a `GetElem` body) and
thus not trivially accessible to `simp` for rewriting. To do this we
drop`GetElem` on `BitVec` as well as `dite` as early as possible in the
pipeline.
This PR optimizes the `ToIR.lean` module, reducing the size of the
compiled C code by a bit over a factor of 3. This significantly improves
the compilation time, making `ToIR` relatively quick to compile.
Closes#8269
This PR lets `cases` fail gracefully when the motive has an complex
argument whose type is dependent type on the targets. While the
`induction` tactic can handle this well, `cases` does not. This change
at least gracefully degrades to not instantiating that motive parameter.
See issue #8296 for more details on this issue.
This PR shows that negating a bitvector created from a natural number
equals creating a bitvector from the the negative of that number (as an
integer).
```lean
theorem neg_ofNat_eq_ofInt_neg {w : Nat} (x : Nat) :
- BitVec.ofNat w x = BitVec.ofInt w (- x) := by
apply BitVec.eq_of_toInt_eq
simp [BitVec.toInt_neg, BitVec.toInt_ofNat]
```
---------
Co-authored-by: Luisa Cicolini <48860705+luisacicolini@users.noreply.github.com>
This PR improves the generation of `.induct_unfolding` by rewriting
`match` statements more reliably, using the new “congruence equations”
introduced in #8284. Fixes#8195.
This PR adds a new variant of equations for matchers, namely “congruence
equations” that generalize the normal matcher equations. They have
unrestricted left-hand-sides, extra equality assumptions relating the
discriminiants with the patterns and thus prove heterogenous equalities.
In that sense they combine congruence with rewriting. They can be used
to rewrite matcher applications where, due to dependencies, `simp` would
fail to rewrite the discriminants, and will be used when producing the
unfolding induction theorems.
This PR optimizes lean_nat_shiftr for scalar operands. The new compiler
converts Nat divisions into right shifts, so this now shows up as hot in
some profiles.
This PR improves the type-as-hole error message. Type-as-hole error for
theorem declarations should not admit the possibility of omitting the
type entirely.
---------
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
This PR changes `addPPExplicitToExposeDiff` to show universe differences
and to visit into projections, e.g.:
```
error: tactic 'rfl' failed, the left-hand side
(Test.mk (∀ (x : PUnit.{1}), True)).1
is not definitionally equal to the right-hand side
(Test.mk (∀ (x : PUnit.{2}), True)).1
```
for
```lean
inductive Test where
| mk (x : Prop)
example : (Test.mk (∀ _ : PUnit.{1}, True)).1 = (Test.mk (∀ _ : PUnit.{2}, True)).1 := by
rfl
```
This PR makes `#guard_msgs` to treat `trace` messages separate from
`info`, `warning` and `error`. It also introduce the ability to say
`#guard_msgs (pass info`, like `(drop info)` so far, and also adds
`(check info)` as the explicit form of `(info)`, for completeness.
Fixes#8266
This PR adjusts the error message when `apply` fails to unify. It is
clearer about distinguishing the term being applied and the goal, as
well as distinguishing the "conclusion" of the given term and the term
itself.
---------
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
This PR rewords the `application type mismatch` error message by more
specifically mentioning that the problem is with the final argument.
This is useful when the same argument is passed to the function multiple
times.
We decided against using a wording which specifically mentions the
"function expression", because users who are not used to currying might
not think of the `f a` in `f a b` as a function.
This PR adds additional infrastructure for error message formatting.
Specifically, it adds convenience formatters for hints and notes,
including the ability to attach code actions to hint messages using a
"Try This"-like widget, along with several convenience formatters for
message data.
---------
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
This PR fixes unintended inlining of `ToJson`, `FromJson`, and `Repr`
instances, which was causing exponential compilation times in `deriving`
clauses for large structures.
This PR omits cases from functional induction/cases principles that are
implemented `by contradiction` (or, more generally, `False.elim`,
`absurd` or `noConfusion). Breaking change in the sense that there are
fewer goals to prove after using functional induction.
Fixes#8103.
This PR avoids an issue where, through other potential bugs, constants
that are tracked by `Kernel.Environment` but not `Environment` are not
persisted.
This PR changes the behaviour of `apply?` so that the `sorry` it uses to
close the goal is non-synthetic. (Recall that correct use of synthetic
sorries requires that the tactic also generates an error message, which
we don't want to do in this situation.) Either this PR or #8230 are
sufficient to defend against the problem reported in #8212.
