Commit 2022-12-20 23:45 8fbf7968

View on Github →

feat: polyrith tactic (#942) The main functionality of polyrith is represented here: it contacts Sagemath to get the coefficients required to pass to linear_combination. TODO:

  • fix docs & lint
  • fix tests
    • There are some auxiliary tactics used to construct test cases for polyrith and perform dry-run testing which does not require contacting sage in CI. Since the mock testing setup is not done yet, you can only test it for real right now, but I don't want to run that in CI for the same reason so currently all the tests are commented out. Most of them are still failing though because of things like a missing instance for CommSemiring Rat or the existence of the Real type entirely.

Estimated changes