Zulip Chat Archive

Stream: new members

Topic: basic class setup and reflexivity


view this post on Zulip Michael Beeson (Sep 06 2020 at 15:56):

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"

view this post on Zulip Reid Barton (Sep 06 2020 at 16:11):

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

view this post on Zulip Michael Beeson (Sep 06 2020 at 16:31):

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.

view this post on Zulip Kevin Buzzard (Sep 06 2020 at 17:02):

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


Last updated: May 11 2021 at 13:22 UTC