Commit 2023-10-26 01:32 452129ae

feat: have notation3 use elaborator when generating matchers, add support for pi/lambda (#6833) 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.