## Stream: new members

### Topic: Can't recurse on existential quantifier in a tactic mode def

#### 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 Prop, right?

#### 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