Zulip Chat Archive

Stream: general

Topic: anonymous hypotheses


view this post on Zulip Rob Lewis (Jul 23 2019 at 13:08):

Heh. @Jasmin Blanchette just showed me this "feature," which I guess comes from the support for bounded quantifiers like ∀ a ∉ s, true.

lemma f (s : set ) (a  s) : true :=
sorry

lemma g (a > 0) : true :=
sorry

#check f
#check g

Last updated: May 15 2021 at 22:14 UTC