Topic: Foreign goal
Yaël Dillies (Oct 22 2021 at 12:00):
I just encountered a really peculiar bug of the infoview. In the following code, at the end of line 43, I have the following goal:
α: Type u _inst_1: fintype α X: α → Profinite s: limits.cocone (discrete.functor X) j: discrete α ⊢ (sigma_cofan X).ι.app j ≫ sigma.desc (λ (a : α), X a) (λ (a : α), s.ι.app a) = s.ι.app j
which is NOT the expected goal:
α : Type u_1, hα : nonempty α, X : α → Type u_2, _inst_1 : Π (a : α), topological_space (X a), hs : is_preconnected ∅, this : (α → ?m_1) → ?m_1 ⊢ ∃ (a : α) (t : set (X a)), is_preconnected t ∧ ∅ = sigma.mk a '' t
The faulty code
Of course, there are lots of errors in the file, but seeing the goal of something that's 40 lines below is odd.
Shing Tak Lam (Oct 22 2021 at 12:17):
Kevin Buzzard (Oct 22 2021 at 12:32):
aah, the famous "line 65 column 33 bug"
Kevin Buzzard (Oct 22 2021 at 12:36):
I see tactic.congr was edited recently, presumably something to do with the port, so now maybe the issue occurs in new positions :-)
Last updated: Aug 03 2023 at 10:10 UTC