Zulip Chat Archive

Stream: general

Topic: Noncomputability poisoning

Yaël Dillies (Jan 27 2022 at 17:06):

What are the prescribed methods against noncomputability poisoning? I thought I had understood it (make computable instances up until the noncomputable one, but then I get https://github.com/leanprover-community/mathlib/runs/4967681933?check_suite_focus=true

Eric Rodriguez (Jan 27 2022 at 17:16):

what do you mean by this?

Yaël Dillies (Jan 27 2022 at 17:19):

It's when TC weakens a noncomputable instance instead of finding the weaker computable one.

Yaël Dillies (Jan 27 2022 at 17:20):

Typically docs#nat.conditionally_complete_linear_order_bot vs docs#nat.linear_order

Eric Wieser (Jan 27 2022 at 17:23):

Is the context #11677?

Eric Wieser (Jan 27 2022 at 17:33):

Is the context #11677?

Yury G. Kudryashov (Jan 28 2022 at 02:52):

You can look at the generated instance (e.g., with pp.all) and see where it took a wrong path. Then you can, e.g., add an explicit high priority instance for this typeclass.

Last updated: Dec 20 2023 at 11:08 UTC