Zulip Chat Archive

Stream: general

Topic: Strange error

Yury G. Kudryashov (Jun 17 2020 at 03:21):

I'm trying to move definitions of all order classes to a dedicated file (I want the definitions to be available before all the theory), and moving code around leads to a strange build error, see https://github.com/leanprover-community/mathlib/runs/778969750

Yury G. Kudryashov (Jun 17 2020 at 03:29):

Even with pp.all true I can't understand why it fails to unify two expressions.

Yury G. Kudryashov (Jun 17 2020 at 03:40):

I don't understand what happens, and can't make an #mwe.

Last updated: Dec 20 2023 at 11:08 UTC