Zulip Chat Archive
Stream: mathlib4
Topic: delta; infer_instance
Yury G. Kudryashov (Feb 01 2023 at 10:50):
I see the pattern delta mydef; infer_instance used here and there. It seems that this proofs inserts id and it's not reducible.
Yury G. Kudryashov (Feb 01 2023 at 10:50):
So, Lean fails to unify some instances.
Yury G. Kudryashov (Feb 01 2023 at 10:50):
What should we use instead? inferInstanceAs?
Yury G. Kudryashov (Feb 05 2023 at 10:29):
Last updated: Dec 20 2023 at 11:08 UTC