Commits on Oct 9, 2024

1. fix: store local context for 'don't know how to synthesize implicit a… …

   …rgument' errors
   
   When named arguments introduce eta arguments, the full application contains fvars for these eta arguments, so `MVarErrorKind.implicitArg` needs to keep a local context for its error messages. The local context of the mvar associated to the `MVarErrorKind` is not sufficient since when an eta argument come after an implicit argument, the implicit argument's mvar doesn't contain the eta argument's fvar in its local context.
   
   Closes leanprover#5475

   

   kmill committed Oct 9, 2024
   Configuration menu

   • View commit details
   • Copy full SHA for e8d358d
   • Browse repository at this point

   Copy the full SHA

   e8d358d View commit details

   Browse the repository at this point in the history