feat: custom elaborators for TangentSpace and tangentMap(Within)#36155
feat: custom elaborators for TangentSpace and tangentMap(Within)#36155grunweg wants to merge 4 commits intoleanprover-community:masterfrom
Conversation
PR summary f3179c596dImport changes for modified filesNo significant changes to the import graph Import changes for all files
Declarations diffNo declarations were harmed in the making of this PR! 🐙 You can run this locally as follows## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>The doc-module for No changes to technical debt.You can run this locally as
|
mathlib-merge-conflicts
bot
added
the
merge-conflict
|
This pull request has conflicts, please merge |
grunweg
force-pushed
the
tangentspace-elaborators
branch
from
7e6190d to
ca1ba65
Compare
grunweg
removed
the
merge-conflict
grunweg
changed the title
ocfnash
left a comment
ocfnash
left a comment
There was a problem hiding this comment.
Modulo ~15 lines of meta code and a question about tests this is all fine.
We'll need to find another reviewer for the meta code though.
| let (srcI, tgtI) ← findModels ef none | ||
| mkAppM ``tangentMap #[srcI, tgtI, ef] | ||
|
|
||
| -- TODO: add tests for the three elaborators above! |
There was a problem hiding this comment.
A comment of the form "TODO add tests" sets off alarm bells for me but maybe this is OK. Do we have tests for other elaborators?
There was a problem hiding this comment.
All the other elaborators (and the underlying mechanism) are very well-tested, so I'm not worried about correctness here. I'm happy to add tests also. I guess Thomas or Patrick might be suitable reviewers for the meta-code. (The implementation is very analogous to the other elaborators.)
4 participants
Uh oh!
There was an error while loading. Please reload this page.