anonymous hypotheses

Stream: general

[Rob Lewis]

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