Zulip Chat Archive

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: Dec 20 2023 at 11:08 UTC