Zulip Chat Archive

Stream: mathlib4

Topic: mathport apply_rules

Yury G. Kudryashov (Feb 05 2023 at 19:20):

Hi @Mario Carneiro , I found another bug in mathport: https://github.com/leanprover-community/mathlib4/blob/8f25f3b7ac1ccfeeaa8f4e5ce963c880437a9f1b/Mathlib/Topology/Algebra/Order/IntermediateValue.lean#L288

Yury G. Kudryashov (Feb 05 2023 at 19:21):

The original line that causes trouble: https://github.com/leanprover-community/mathlib/blob/master/src/topology/algebra/order/intermediate_value.lean#L281

Mario Carneiro (Feb 05 2023 at 22:42):

that kind of bug usually means that the syntax of the lean 3 tactic has changed

Last updated: Dec 20 2023 at 11:08 UTC