Stream: new members
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"
Reid Barton (Sep 06 2020 at 16:11):
Lean needs some way to know what
c you're talking about. For example,
(c : K) = c should work.
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.
Kevin Buzzard (Sep 06 2020 at 17:02):
c : K without parentheses is not valid syntax.
Last updated: May 11 2021 at 13:22 UTC