Stream: Coq users

Topic: hypothesis


view this post on Zulip zohaze (May 01 2023 at 15:12):

H : given_point a b (x :: t)
eq1 : nos = 0
IHimg' : given_point a b  t -> false = true

Are these two hypothesises false?

view this post on Zulip Laurent Théry (May 01 2023 at 15:19):

What is given_point, what is nos?

view this post on Zulip zohaze (May 02 2023 at 13:22):

given_point is function's name, nos a b :nat

view this post on Zulip Laurent Théry (May 02 2023 at 14:04):

If you manage to prove that given_point a b (x :: t) -> given_point a b t yes there is a contradiction, otherwise no


Last updated: Jun 24 2024 at 00:02 UTC