Due to nested recursion, we do two passes of `getRecArgInfo`: One on
each argument in isolation, to see which inductive types are around
(e.g. `Tree` and `List`), and
then we later refine/replace this result with the data for the nested
type former (the implicit `ListTree`).
If we have nested recursion through a non-recursive data type like
`Array` or `Prod` then arguemnts of these types should survive the first
phase, so that we can still use them when looking for, say, `Array
Tree`.
This was helpfully reported by @arthur-adjedj.
For every parenthesized expression `(foo)`, the InfoView produces an
interactive component both for `(foo)` itself and its subexpression
`foo` because the corresponding `TaggedText` in the language server is
duplicated as well. Both of these subexpressions have the same
subexpression position and so they are identical w.r.t. interactive
features.
Removing this duplication would help reduce the size of the DOM of the
InfoView and ensure that the UI for InfoView features is consistent for
`(foo)` and `foo` (e.g. hovers would always highlight `(foo)`, not
either `(foo)` or `foo` depending on whether the mouse cursor is on the
bracket or not). It would also help resolve a bug where selecting a
subexpression will yield selection highlighting both for `(foo)` and
`foo`, as we use the subexpression position to identify which terms to
highlight.
This PR adjusts the parenthesizer to move the corresponding info instead
of duplicating it.
Draft of adding ci workflow using lean-action on `lake new/init`
This PR is currently missing lake options for the user to control this
feature.
Closes#4606
---------
Co-authored-by: Mac Malone <tydeu@hatpress.net>
When resolving anonymous dot notation (`.ident x y z`), it would reduce
the expected type to whnf. Now, it unfolds definitions step-by-step,
even if the type synonym is for a pi type like so
```lean
def Foo : Prop := ∀ a : Nat, a = a
protected theorem Foo.intro : Foo := sorry
example : Foo := .intro
```
Closes#4761
After each tactic step, we save the info tree created by it together
with an appropriate info tree context that makes it stand-alone (which
we already did before to some degree, see `Info.updateContext?`). Then,
in the adjusted request handlers, we first search for a snapshot task
containing the required position, if so wait on it, and if it yielded an
info tree, use it to answer the request, or else continue searching and
waiting, falling back to the full info tree, which should be unchanged
by this PR.
The definition header does *not* report info trees early as in general
it is not stand-alone in the tactic sense but may contain e.g.
metavariables solved by the body in which case we do want to show the
ultimate state as before. This could be refined in the future in case
there are no unsolved mvars.
The adjusted request handlers are exactly the ones waited on together by
the info view, so they all have to be adjusted to have any effect on the
UX. Further request handlers may be adjusted in the future.
No new tests as "replies early" is not something we can test with our
current framework but the existing test suite did help in uncovering
functional regressions.
previously, `#eval` would happily evaluate expressions that contain
`sorry`, either explicitly or because of failing tactics. In conjunction
with operations like array access this can lead to the lean process
crashing, which isn't particularly great.
So how `#eval` will refuse to run code that (transitively) depends on
the `sorry` axiom (using the same code as `#print axioms`).
If the user really wants to run it, they can use `#eval!`.
Closes#1697
This PR updates the screenshots and instructions in the quickstart guide
for the most recent Lean 4 VS Code extension version and makes a small
stylistic change suggested by @semorrison.
The `elab_as_elim` elaborator eagerly elaborates arguments that can help
with elaborating the motive, however it does not include the transitive
closure of parameters appearing in types of parameters appearing in ...
types of targets.
This leads to counter-intuitive behavior where arguments supplied to the
eliminator may unexpectedly have postponed elaboration, causing motives
to be type incorrect for under-applied eliminators such as the
following:
```lean
class IsEmpty (α : Sort u) : Prop where
protected false : α → False
@[elab_as_elim]
def isEmptyElim [IsEmpty α] {p : α → Sort _} (a : α) : p a :=
(IsEmpty.false a).elim
example {α : Type _} [IsEmpty α] :
id (α → False) := isEmptyElim (α := α)
```
The issue is that when `isEmptyElim (α := α)` is computing its motive,
the value of the postponed argument `α` is still an unassignable
metavariable. With this PR, this argument is now among those that are
eagerly elaborated since it appears as the type of the target `a`.
This PR also contains some other fixes:
* When underapplied, does unification when instantiating foralls in the
expected type.
* When overapplied, type checks the generalized-and-reverted expected
type.
* When collecting targets, collects them in the correct order.
Adds trace class `trace.Elab.app.elab_as_elim`.
This is a followup to #4722, which added motive type checking but
exposed the eagerness issue.
Also extends existing definition for `getScope`/`getScopes` and
clarifies that the `end` command is optional at the end of a file.
---------
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
The original idea was to use `bif` in computation contexts and `if` in
propositional contexts, but this turned out to be really inconvenient in
practice.
code to create nested `PProd`s, and project out, and related functions
were scattered in variuos places. This unifies them in
`Lean.Meta.PProdN`.
It also consistently avoids the terminal `True` or `PUnit`, for slightly
easier to read constructions.
This refactoring PR changes the structure of the `FunInd` module, with
the main purpose to make it easier to support mutual structural
recursion.
In particular the recursive calls are now longer recognized by their
terms (simple for well-founded recursion, `.app oldIH [arg, proof]`, but
tedious for structural recursion and even more so for mutual structural
recursion), but the type after replacing `oldIH` with `newIH`, where the
type will be simply and plainly `mkAppN motive args`).
We also no longer try to guess whether we deal with well-founded or
structural recursion but instead rely on the `EqnInfo` environment
extensions. The previous code tried to handle both variants, but they
differ too much, so having separate top-level functions is easier.
This also fuses the `foldCalls` and `collectIHs` traversals and
introduces a suitable monad for collecting the inductive hypotheses.
This is part 2 of 2 of #4801 (which closes#4654). That PR was split in
two to allow a stage0 update between declaring the `usize` functions and
using them where they are needed.
Add efficient `usize` functions for `Array`, `ByteArray`, `FloatArray`.
This is part 1 of 2 since there is a need to update stage0 between the
two parts. (See discussion below.)
Closes#4654
Changes:
- We avoid the thread local storage.
- We use a hash map to ensure that cached values are not lost.
- We remove `check_system`. If this becomes an issue in the future we
should precompute the remaining amount of stack space, and use a cheaper
check.
- We add a `Expr.replaceImpl`, and will use it to implement
`Expr.replace` after update-stage0
