Zulip Chat Archive

Stream: general

Topic: anonymous hypotheses


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: Dec 20 2023 at 11:08 UTC