Zulip Chat Archive

Stream: triage

Topic: PR #17142: fix(tactic/polyrith): fix crash when hypothese...


Random Issue Bot (Jan 29 2023 at 14:08):

Today I chose PR 17142 for discussion!

fix(tactic/polyrith): fix crash when hypotheses are constant polynomials
Created by @Eric Wieser (@eric-wieser) on 2022-10-25
Labels: bug, t-meta

Is this PR still relevant? Any recent updates? Anyone making progress?

Eric Wieser (Jan 29 2023 at 16:06):

This probably needs forward-porting to mathlib4, I suspect no one will ever have time to review the mathlib3 version

Kevin Buzzard (Jan 29 2023 at 16:08):

@Rob Lewis do you have any comments on this?


Last updated: Dec 20 2023 at 11:08 UTC