Internal error

Stream: new members

[Kevin Sullivan]

Error updating: Error fetching goals: Rpc error: InternalError: unknown metavariable '?_uniq.152'.

This error is produced by the following code. Lean nightly from 8/30. Haven't tried most recent build. Class started with this version in fall and has stuck with it.

import Mathlib.Data.Set.Basic

example (α : Type) (r s t : Set α) : (r ∩ (s ∪ t)) = ((r ∩ s) ∪ (r ∩ t)) := by
    apply Set.ext   -- replaces = with logical ↔
    intro x
    apply Iff.intro
    intro h
    cases h with
    | intro hl hr =>
      _

[Kyle Miller]

In a recent mathlib, I'm not seeing anything but the "unsolved goals" error. Where is it being reported for you?

[Kevin Sullivan]

Kyle Miller said:

In a recent mathlib, I'm not seeing anything but the "unsolved goals" error. Where is it being reported for you?

Let me pull the most recent and I'll get back. Thank you.

[Kevin Sullivan]

Kevin Sullivan said:

Kyle Miller said:

In a recent mathlib, I'm not seeing anything but the "unsolved goals" error. Where is it being reported for you?

Let me pull the most recent and I'll get back. Thank you.

All good with most recent.