This is something we can do to make our annotations more robust in the future: right now we have quite a few #rocq_ignore statements which say to "use synthesis", or something like it. It might be better to state which typeclass we expect to exist, under which circumstances, and have the ignore statement perform the synthesis to double check.
This is something we can do to make our annotations more robust in the future: right now we have quite a few
#rocq_ignorestatements which say to "use synthesis", or something like it. It might be better to state which typeclass we expect to exist, under which circumstances, and have the ignore statement perform the synthesis to double check.