Zulip Chat Archive

Stream: mathlib4

Topic: Parsing error

Yaël Dillies (Jan 11 2023 at 21:58):

There's something wrong with the parsing in mathlib4#1080, but I have no idea why. Just spent the last 15min trying random things and it always tells me "expected command". Could someone investigate?

Mario Carneiro (Jan 11 2023 at 22:52):

Where? On what?

Yaël Dillies (Jan 12 2023 at 00:17):

In data.int.order.basic, line 68.

Yaël Dillies (Jan 12 2023 at 00:18):

I don't know what it's on. It looks like it's still parsing one declaration before going to the next

Damiano Testa (Jan 12 2023 at 00:30):

Have you tried moving the by to the previous line? :shrug:

Mario Carneiro (Jan 12 2023 at 00:40):

I can't reproduce. The only error I get is

./././Mathlib/Data/Int/Order/Basic.lean:68:20: error: unknown identifier 'cast_coe_nat'
./././Mathlib/Data/Int/Order/Basic.lean:68:20: error: tactic 'rewrite' failed, equality or iff proof expected
  ?m.3342
α : Type u_1
inst✝ : AddGroupWithOne α
n : ℤ
⊢ ↑(natAbs n) = ↑↑(natAbs n)

Mario Carneiro (Jan 12 2023 at 00:41):

and CI seems to agree

Last updated: May 02 2025 at 03:31 UTC