Sebastian Ullrich
Sebastian Ullrich
It would be good to first look at whether support for the combination of out-params and coercions cannot be improved in general. There already is special handling for out-params in...
The following patch should fix the underlying issue, could you test it? ```diff --- a/src/Lean/Elab/Frontend.lean +++ b/src/Lean/Elab/Frontend.lean @@ -102,7 +102,7 @@ partial def IO.processCommandsIncrementally (inputCtx : Parser.InputContext) where go initialSnap...
My bad, could you try the above fix with this line instead? ``` let trees := commands.map (·.finishedSnap.get.infoTree?) |>.filterMap id |>.toPArray' ```
Thanks for testing, addressed in https://github.com/leanprover/lean4/pull/5763
The Nix build has been officially deprecated #4895
Must be a general info tree issue 
I think we're still missing a tactic version of #1396
Let's first see if it builds at all
(seems to have created some issues with partial syntax trees in the test. Resolving this is not highest prio for me at the moment)
> > are instance-implicit variables that reference any variable included by these rules. > > Should this be "are instance-implicit variables and all referenced variables are included by these rules."?...