This PR simplifies the signature of `Array.mapIdx`, to take a function
`f : Nat \to \a \to \b` rather than a function `f : Fin as.size \to \a
\to \b`.
Lean doesn't actually use the extra generality anywhere (so in fact this
change *simplifies* all the call sites of `Array.mapIdx`, since we no
longer need to throw away the proof).
This change would make the function signature equivalent to
`List.mapIdx`, hence making it easier to write verification lemmas.
We keep the original behaviour as `Array.mapFinIdx`.
This solves the issue where certain subexpressions are lacking syntax
hovers because the hover text is not "builtin" - it only shows up if the
`Parser` constant is imported in the environment. For top level syntaxes
this is not a problem because `builtin_term_parser` will automatically
add this doc information, but nested syntaxes don't get the same
treatment.
We could walk the expression and add builtin docs recursively, but this
is somewhat expensive and unnecessary given that it's a fixed list of
declarations in lean core. Moreover, there are reasons to want to
control which syntax nodes actually get hovers, and while a better
system for that is forthcoming, for now it can be achieved by
strategically not applying the `@[builtin_doc]` attribute.
Fixes#3842
This fixes an issue where the completion would use info nodes before the
cursor for computing completions.
Fixes https://github.com/leanprover/lean4/issues/3462.
ToDo:
- [x] Fix test failures for completions that previously worked by
accident (cc: @Kha)
- [x] stage0 update
---------
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
This coercion caused difficult-to-diagnose bugs sometimes. Because there
are some situations where converting a string to a name should be done
by parsing the string, and others where it should not, an explicit
choice seems better here.
---------
Co-authored-by: Mac Malone <tydeu@hatpress.net>
We use `nullKind` for the `group` parser combinator.
When pattern matching `nullKind` nodes, we check their arities.
So, error recovery often fails for parsers that use the `group`
combinator.
For example, we have the parser
```
def whereDecls := leading_parser "where " >> many1Indent (group (letRecDecl >> optional ";"))
```
If there is syntax error at `letRecDecl`, the node corresponding to
```
group (letRecDecl >> optional ";")
```
will contain only one child, and the pattern matching at
```
def expandWhereDecls (whereDecls : Syntax) (body : Syntax) : MacroM Syntax :=
match whereDecls with
| `(whereDecls|where $[$decls:letRecDecl $[;]?]*) => `(let rec $decls:letRecDecl,*; $body)
| _ => Macro.throwUnsupported
```
fails, and we can't elaborate the partial syntax tree for
`letRecDecl`, and auto-completion will not work there.
We address this issue by using a new kind for the `group` combinator.
The idea is to pattern match `group` as we pattern match `node`s with
proper syntax node kinds. This change is consistent with the way we
use `group` where it mainly a convenience for saving us the trouble of
defining a new parser definition that is used only once.
@Kha I had some unexpected surprises, but it is a good change.
Here is the summary.
1- We could get rid of `a %ₙ b` and `ModN` class. We can use `HMod`
instead. It was a positive surprise since I didn't remember we had
this `ModN` class.
2- Coercions are never used in heterogeneous operators. This is
expected since `a * b` is now notation for `HMul.hMul a b`, and
`a` and `b` may have different types. I manually added instances such
as `HMul Nat Int Int`. However, I did not try to add generic instances
such as
```
instance [Coe a b] [Mul b] : HMul a b b where
hMul x y := mul (coe x) y
```
I will try later.
3- Give `h : cs.size > 0`, I got a type error at
```
let idx : Fin cs.size := ⟨cs.size - 1, Nat.predLt h⟩
```
`Nat.predLt h` has type `Nat.pred cs.size < cs.size`
However, `Nat.pred cs.size` doesn't unify with `cs.size - 1`.
The problem is that we can't synthesize the `HSub` instance until
we apply the default instances.
It worked before because `isDefEq` would force the pending TC
problem `Sub Nat` to be resolved, and after that we would be able
to reduce `cs.size - 1` and establish that it is definitionally
equal to `Nat.pred cs.size`.
I considered two possible workarounds
a) `let idx : Fin cs.size := ⟨cs.size - (1:Nat), Nat.predLt h⟩`
b) `let idx : Fin cs.size := ⟨cs.size - 1, by exact Nat.predLt h⟩`
The first one works because we are not providing enough information
for synthesizing the `HSub` instance. The second works because it
postpones the elaboration of `Nat.predLt h`. The default instances
will be applied before we start applying tactics.
4- The `.` notation is affected too. For example, `(x + 1).toUInt8`
doesn't work since we don't know the type of `x+1` until we apply
default instances. I fixed it by using `(x + (1:Nat)).toUInt8`.
Another possible fix is `Nat.toUInt8 (x + 1)`.
Similarly, `(x+1).fold ...` doesn't work.
5- The following code failed to be elaborated
```
indent (push s!"{ss'}\n") (some (0 - Format.getIndent (← getOptions)))
```
It was working before, but it relied on how the expected type is
propagated. The elaborator process
```
some (0 - Format.getIndent (← getOptions))
```
with expected type `(Option Int)`. So, the `-` is interpreted as
`Int.sub` although `Format.getIndent (← getOptions)` has type `Nat`.
In the new `HSub`, the expected type doesn't really influence TC
resolution since it is an `outparam`. So, we failed with the error
failed to synthesize `HSub Nat Nat Int`.
One possible fix was to add the instance `HSub Nat Nat Int` with
`Int.sub`, but I used the following fix
```
some ((0 : Int) - Format.getIndent (← getOptions))
```
which makes it clear that we want the `Int.sub` operator instead of
`Nat.sub`.
