## Stream: general

### Topic: unfolding from cases

#### Reid Barton (Nov 28 2018 at 14:31):

def x : ℕ := 1 + 1 + 1 + 1

inductive P : ℕ → Type
| p : P x

example {a} (h : P a) : a = 4 := begin
cases h,
end


Goal is ⊢ nat.succ (nat.add (1 + 1 + 1) 0) = 4. Is all this unfolding expected? I wanted x = 4.

#### Kenny Lau (Nov 28 2018 at 14:50):

interestingly induction h produces the expected x = 0:

def x : ℕ := 0

inductive P : ℕ → Type
| p : P x

example {a} (h : P a) : a = 0 := begin
induction h,
end


Last updated: May 14 2021 at 02:15 UTC