Zulip Chat Archive

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) :  :=
  cases h,

--this does...
def f (h :  x : , true) : true :=
  cases h,

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