Stream: Miscellaneous

Topic: Coqhammer

view this post on Zulip Patrick Nicodemus (Apr 16 2023 at 15:56):

I tried to prove this with Coqhammer:

Theorem abc2 : exists k : nat * nat, fst k = 0 /\ snd k = 3

and it failed. I am wondering what the problem is here, is it with the use of product types?

view this post on Zulip Notification Bot (Apr 16 2023 at 17:28):

This topic was moved to #Coq users > Coqhammer by Karl Palmskog.

Last updated: Nov 29 2023 at 21:01 UTC