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

Stream: new members

[ROCKY KAMEN-RUBIO]

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]

the error says something about only eliminating into Prop, right?

[Bryan Gin-ge Chen]

This thread has some nice explanations.

[Kenny Lau]

it's not a bug it's a feature

[Jalex Stark]

I was about to post the same link! I appreciate that the thread has an easy to remember name