basic class setup and reflexivity

Stream: new members

[Michael Beeson]

class  Model4 (K:Type)  :=
(c:K)

open Model4
variables (K:Type) [Model4 K] (x:K)

lemma test6: ∀ x:K, x=x :=
  assume x,
  begin
    reflexivity,
  end

lemma test7: c=c :=
  begin
    reflexivity,
  end

test6 works fine, showing that the basic setup is OK, but test7 fails,
"don't know how to synthesize placeholder"

[Reid Barton]

Lean needs some way to know what K's c you're talking about. For example, (c : K) = c should work.

[Michael Beeson]

Thank you Reid. I tried that before, but without the parentheses. That is, c:K = c does not work, but (c:K) = c does work, as you said.

[Kevin Buzzard]

I think c : K without parentheses is not valid syntax.