Stream: new members
ROCKY KAMEN-RUBIO (Jun 28 2020 at 05:30):
Could someone help shed some light on this behavior?
import data.nat.basic import tactic --this doesn't work def f (h : ∃ x : ℕ, true) : ℕ := begin cases h, sorry end --this does... def f (h : ∃ x : ℕ, true) : true := begin cases h, sorry end
Jalex Stark (Jun 28 2020 at 05:31):
the error says something about only eliminating into
Bryan Gin-ge Chen (Jun 28 2020 at 05:32):
This thread has some nice explanations.
Kenny Lau (Jun 28 2020 at 05:32):
it's not a bug it's a feature
Jalex Stark (Jun 28 2020 at 05:32):
I was about to post the same link! I appreciate that the thread has an easy to remember name
Last updated: May 12 2021 at 04:19 UTC