Zulip Chat Archive

Stream: new members

Topic: getting more information on an error

Michael Beeson (Oct 06 2020 at 21:13):

I know there is a way to get a more elaborate error message but I have forgotten what it is. I have the following error that is
mysterious to me. It complains about the type of "a" but I don't see anything wrong. It is complaining at
this input line:

     have h50: ∀ (p q:M), p ∈ USC a → q ∈ USC a → ¬ p = q → (p ∩ q = Λ ) :=

and here is the error:

M: Type
_inst_1: Model M
mn: M
h1: m ∈ 𝔽
h2: n ∈ 𝔽
h4copy: ∃ (u : M), u ∈ exp M n
b: M
h5: USC b ∈ n
h6: ∃ (u : M), u ∈ n
h7: m ≤ n ↔ ∀ (b : M), b ∈ n → (∃ (a : M), a ∈ m ∧ a ⊆ b ∧ b = (a ∪ b - a))
h3: USC b ∈ n → (∃ (a : M), a ∈ m ∧ a ⊆ USC b ∧ USC b = (a ∪ USC b - a))
x: M
h21: x ⊆ USC b
h22: USC b = (x ∪ USC b - x)
a: M := union x
h9: a = union x
line789: x = USC a
h20: USC a ∈ m
h23: (∃ (a : M), USC a ∈ m) ↔ ∃ (b : M), b ∈ exp M m
h24: ∃ (a : M), USC a ∈ m
bFinite: b ∈ FINITE M
xFinite: USC a ∈ FINITE M
h40: ∀ (u : M), u ∈ USC a → u ∈ FINITE M
⊢ a ∈ FINITE M
All Messages (1)
inf7.lean:1163:8
type mismatch at application
  USC a
term
  a
has type
  p ∈ USC a : Prop
but is expected to have type
  M : Type