I was about to to address the TODO
/- TODO: check arity of the given function. If it takes a PSigma as the
last argument,
this function will produce incorrect results. -/
because we now have an arity-observing variant of `decodePackedArg?` in
`unpackArg` in `PackMutual`, and it would be prudent to use it here.
But I first wanted to create a test case that would actually exhibit
this corner case, and failed.
This code was added in 096e4eb6d0 and it had a test case, but not even
that test case seems to be actually using the `decodePackedArg?`
function, neither back then nor now.
Also, mathlib works without this code.
So this seems to be dead code, possibly due to other changes to the
system, and thus can be removed. A strategically place comments points
back to this PR in case we need to resurrect that code.
The pattern
```
for h : i in [:xs.size] do
let x := xs[i]'h.2
```
is occassionally useful to iterate over an array with the index in
hand. This PR extends the `get_elem_tactic_trivial` so that one can
simply write
```
for h : i in [:xs.size] do
let x := xs[i]
```
fixes#3032.
This removes checks in `Lean.Meta.reduceNat?` that caused it to fail on
terms it could handle because they contain meta variables in arguments.
This lead to those operations being reduced using their equational
definitions and slow performance on large patterns:
```
set_option profiler true
set_option profiler.threshold 1
def testMod (x:Nat) :=
match x with
| 128 % 1024 => true
| _ => false
-- elaboration took 3.02ms
def testMul (x:Nat) :=
match x with
| 128 * 1 => true
| _ => false
-- type checking took 11.1ms
-- compilation of testMul.match_1 took 313ms
-- compilation of testMul took 65.7ms
-- elaboration took 58.9ms
```
Performance is slower on `testMul` than `testMod` because `whnf` ends up
evaluateing `128 * 1` using Peano arithmetic while `128 % 1024` is able
to avoid that treatment since `128 < 1024`.
This makes hover info, go to definition, etc work for the `h` in `cases
h : e`. The implementation is similar to that used for the `generalize h
: e = x` tactic.
# Summary
This makes a small addition to our take on the LSP protocol
in the form of supporting snippet text edits.
It has been discussed
[here](https://github.com/microsoft/language-server-protocol/issues/592)
on the LSP issue tracker for a while,
but seems unlikely to be added anytime soon.
This feature was requested by @PatrickMassot for the purposes
of supporting Lean code templates in code actions and widgets.
---------
Co-authored-by: David Thrane Christiansen <david@davidchristiansen.dk>
There were no `quot_precheck` instances registered for the expression
tree elaborators, which prevented them from being usable in a `notation`
expansion without turning off the quotation prechecker.
Users can evaluate whether `set_option quotPrecheck false` is still
necessary for their `notation` definitions.
Switches from encoding `let_fun` using an annotated `(fun x : t => b) v`
expression to a function application `letFun v (fun x : t => b)`.
---------
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
Fixes reference implementation of `ByteArray.copySlice`, as reported
https://github.com/leanprover/lean4/issues/2966.
Adds tests.
---------
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
If a user deleted `lakefile.olean` manually without deleting
`lakefile.olean.lock`, Lake would still attempt to load it and thus
produce an error. Now it should properly re-elaborate the configuration
file.
This adds a `test_extern` command.
Usage:
```
import Lean.Util.TestExtern
test_extern Nat.add 17 37
```
This:
* Checks that the head symbol has an `@[extern]` attribute.
* Writes down `t == t'`, where `t` is the term provided, and `t'` is the
reference implementation (specifically, `t` with the head symbol
unfolded).
* Tries to reduce this to `true`, and complains if this fails.
Note that the type of the term must have a `BEq` instance for this to
work: there's a self-explanatory error message if it isn't available.
This definition was clearly meant to be in the `List` namespace, but it
is also in a `namespace Lean` so it ended up as `Lean.List.toSMap`
instead of `List.toSMap`. It would be nice if #3031 made this
unnecessary, but for now this seems to be the convention.
I noticed this because of another side effect: it defines `Lean.List` as
a namespace, which means that
```lean
import Std
namespace Lean
open List
#check [1] <+ [2]
```
does not work as expected, it opens the `Lean.List` namespace instead of
the `List` namespace. Should there be a regression test to ensure that
the `Lean.List` namespace (and maybe others) are not accidentally
created? (Unfortunately this puts a bit of a damper on #3031.)
Fixes an issue reported on Zulip; see the test case.
* Modifies the `MonadBacktrack` instance for `SimpM` to also backtrack
the `UsedSimps` field.
* When calling the discharger, `saveState`, and then `restoreState` if
something goes wrong.
I'm not certain that it makes sense to restore the `MetaM` state if
discharging fails. I can easily change this to more conservatively just
backtrack the `UsedSimps` after failed discharging.
Changes the implementation of `List.all` and `List.any` so they
short-circuit. The implementations are tail-recursive.
This replaces https://github.com/leanprover/std4/pull/392, which was
going to do this with `@[csimp]`.
until around 7fe6881 the way to define well-founded recursions was to
specify a `WellFoundedRelation` on the argument explicitly. This was
rather low-level, for example one had to predict the packing of multiple
arguments into `PProd`s, the packing of mutual functions into `PSum`s,
and the cliques that were calculated.
Then the current `termination_by` syntax was introduced, where you
specify the termination argument at a higher level (one clause per
functions, unpacked arguments), and the `WellFoundedRelation` is found
using type class resolution.
The old syntax was kept around as `termination_by'`. This is not used
anywhere in the lean, std, mathlib or the theorem-proving-in-lean
repositories,
and three occurrences I found in the wild can do without
In particular, it should be possible to express anything that the old
syntax
supported also with the new one, possibly requiring a helper type with a
suitable instance, or the following generic wrapper that now lives in
std
```
def wrap {α : Sort u} {r : α → α → Prop} (h : WellFounded r) (x : α) : {x : α // Acc r x}
```
Since the old syntax is unused, has an unhelpful name and relies on
internals, this removes the support. Now is a good time before the
refactoring that's planned in #2921.
The test suite was updated without particular surprises.
The parametric `terminationHint` parser is gone, which means we can
match on syntax more easily now, in `expandDecreasingBy?`.
The elaborator is prone to duplicate terms, including recursive calls,
even if the user only wrote a single one. This duplication is wasteful
if we run the tactics on duplicated calls, and confusing in the output
of GuessLex. So prune the list of recursive calls, and remove those
where another call exists that has the same goal and context that is no
more specific.
Implements "gaps" in string literals. These are escape sequences of the
form `"\" newline whitespace+` that have the interpretation of an empty
string. For example,
```
"this is \
a string"
```
is equivalent to `"this is a string"`. These are modeled after string
continuations in
[Rust](https://doc.rust-lang.org/beta/reference/tokens.html#string-literals).
Implements RFC #2838
before code like
def dup (a : Nat) (b : Nat := a) := a + b
def rec : Nat → Nat
| 0 => 1
| n+1 => dup (dup (dup (rec n)))
decreasing_by decreasing_tactic
would run the `decreasing_tactic` 8 tims, because the recursive call
`rec n` gets duplicate due to the default paramter. Similar effects can
be observed due to dependent types or tactics like `cases`.
This is wasteful, and is confusing to the user when they use
`decreasing_by` interactively. Therfore, we now go through the proof
obligations (MVars) and if solving one would imply solving another one,
we assign the mvars to each other accordingly.
This PR is a sibling of #3004.
I found the documentation page hard to parse, so I figured I should fix
this. It's mostly indentation (e.g. in lists), some line breaks and
making URLs clickable.
With
set_option showInferredTerminationBy true
this prints a message like
Inferred termination argument:
termination_by
ackermann n m => (sizeOf n, sizeOf m)
it tries hard to use names that
* match the names that the user used, if present
* have no daggers (so that it can be copied)
* do not shadow each other
* do not shadow anything from the environment (just to be nice)
it does so by appending sufficient `'` to the name.
Some of the emitted `sizeOf` calls are unnecessary, but they are needed
sometimes with dependent parameters. A follow-up PR will not emit them
for non-dependent arguments, so that in most cases the output is pretty.
Somewhen down the road we also want a code action, maybe triggered by
`termination_by?`. This should come after #2921, as that simplifies that
feature (no need to merge termination arguments from different cliques
for example.)
