Zulip Chat Archive

Stream: new members

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


view this post on Zulip 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

view this post on Zulip Jalex Stark (Jun 28 2020 at 05:31):

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

view this post on Zulip Bryan Gin-ge Chen (Jun 28 2020 at 05:32):

This thread has some nice explanations.

view this post on Zulip Kenny Lau (Jun 28 2020 at 05:32):

it's not a bug it's a feature

view this post on Zulip 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