Zulip Chat Archive

Stream: new members

Topic: Unexpected meta goals

Vasily Ilin (Nov 04 2022 at 20:00):

Why does the below generate meta goals?

import data.polynomial
open polynomial
variables {R : Type} [comm_ring R]

example (n : ) : (n + X.nat_degree  n + 1) :=
  have : X.nat_degree  1,
  -- have 4 goals now!

Ruben Van de Velde (Nov 04 2022 at 20:04):

It doesn't realise what X's base ring is

Ruben Van de Velde (Nov 04 2022 at 20:06):

So have : (X : R[X]).nat_degree..., or just continue and see if lean can figure them out on its own

Damiano Testa (Nov 04 2022 at 21:24):

Also, looking at the code that you posted, I would guess that you intended the X in the statement to be in R[X], but I think that Lean guesses ℕ[X].

(All this is very speculative, of course.)

Last updated: Dec 20 2023 at 11:08 UTC