[Merged by Bors] - feat: have notation3 use elaborator when generating matchers, add support for pi/lambda

[kmill]

notation3 was generating matchers directly from syntax, which included a half-baked implementation of a term elaborator. This switches to elaborating the term and then generating matchers from the elaborated term. This

1. is more robust and consistent, since it uses the main elaborator and one can make use of other notations
2. has the nice side effect of adding term info to expansions in the notation3 command
3. can unfortunately generate matchers that are more restrictive than before since they also match against elaborated features such as implicit arguments.

We now also generate matchers for expansions that have pi types and lambda expressions.

---

[kmill]

@digama0 Here's something you'd suggested during the review of the first implementation of the notation3 delaborator. I've spot-checked that notation3 notation still works with this, though there's one case involving Funlike.coe that generates a too-restrictive matcher (I've left a TODO).

[PatrickMassot]

Thanks a lot for all your work on this!
bors merge

[bors]

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build
• Check all files imported
• Lint style