Ambiguous app elaboration now keeps full info context (
ac0f56e)
Lean’s app elaborator now wraps ambiguous elaboration results in choice info trees that preserve command context and partial term info. That fixes missing metavariable/context data in the infoview for ambiguous syntax and closes #8108.
Lake primitive target list expanded (
2a5b1a2)
lake check now treats several more names as primitives, including Nat, String, Char, and the parameter-related builtins optParam, autoParam, semiOutParam, and outParam. This makes the primitive coverage more complete for challenge/check workflows.
Other misc changes
- None