the code stumbled over recursive functions whose type doesn’t have
enough manifest foralls, like:
```
def FunType := Nat → Nat
mutual
def foo : FunType
| .zero => 0
| .succ n => bar n
def bar : FunType
| .zero => 0
| .succ n => foo n
end
termination_by foo n => n; bar n => n
```
This can be fixed by using `whnf` in appropriate places, to expose the
`.forall` constructor.
Fixes#2925, comes with test case.
`script/most-recent-nightly-tag.sh` determines the most recent nightly
release in your current git history.
Previously it was assuming that you had a `nightly` remote, to pull tags
from. Now it just pulls directly from the repository by URL.
This only really shows up when the `decreasing_tactic` fails with
multiple goals, as in
```
macro_rules
| `(tactic|decreasing_tactic) => `(tactic| by_cases (2 > 1))
def foo (n : Nat) : Nat := foo (n - 1)
termination_by foo n => n
```
where we now get
```
unsolved goals
case inl
n: Nat
h✝: 2 > 1
⊢ (invImage (fun a => a) instWellFoundedRelation).1 (n - 1) n
case inr
n: Nat
h✝: ¬2 > 1
⊢ (invImage (fun a => a) instWellFoundedRelation).1 (n - 1) n
```
rather than
```
LeanProject.lean:3:27
unsolved goals
case inl
n: Nat
h✝: 2 > 1
⊢ (invImage (fun a => a) instWellFoundedRelation).1 (n - 1) n
LeanProject.lean:3:27
unsolved goals
case inr
n: Nat
h✝: ¬2 > 1
⊢ (invImage (fun a => a) instWellFoundedRelation).1 (n - 1) n
```
The effect is neglectible, but the code is a bit nicer, so why not,
before someone looks at it again and wonders whether the goals are
reported separately for a reason.
Some beginners have trouble finding the `if h : c then t else e`
(`dite`) version of `ite`. This augments `ite`'s docstring to mention
the dependent version.
This implements a request handler for the `textDocument/rename` LSP
request, enabling renames via F2. It handles both local renames (e.g.
`let x := 1; x` to `let y := 1; y`) as well as global renames
(definitions).
Unfortunately it does not work for "orphan" files outside a project, as
it uses ilean data for the current file and this does not seem to be
saved for orphan files. As a result, the test file does not work,
although one can manually test the implementation against a project such
as mathlib. (This issue already exists for the "references" request,
e.g. ctrl click on the first `x` in `let x := 1; x` takes you to the
second one only if you are not in an orphan file.)
* Fixesleanprover-community/mathlib4#7124
Modifies `cleanup` so that it takes (1) an array of additional fvarids
to preserve and (2) a flag to control whether to include indirect
propositions.
(This is wanted in mathlib for the `extract_goal` tactic.)
previously, it would ignore a recursive call that has extra arguments,
which can happen when the recursive functions return something of
function type. Therefore just leave them extra arguments in place.
Fixes#2883.
In the previous doc-string, the sentence
> "If any of the selected tactic applications fail, it will call
`failed` with the main goal mvar."
was false both for `Location.wildcard` (where it should have said "If
all", not "If any") or for `Location.targets` (where `failed` is never
called).
Add documentation comments with examples to `universe`, `open`,
`export`, and `variable`.
The documentation shows up when hovering over keywords, hopefully
improving the experience for beginners.
