Stream: Coq users

Topic: natural number


view this post on Zulip pianke (Jul 04 2023 at 18:08):

a =? a - 1 = false.

To prove this i have to put condition on a because natural number start from a (otherwise i will get 0=-1)

view this post on Zulip Emilio Jesús Gallego Arias (Jul 04 2023 at 18:11):

Hi @pianke , a bit of context is missing from your question, but indeed if a is of type nat, there is a problem when a = 0

view this post on Zulip Emilio Jesús Gallego Arias (Jul 04 2023 at 18:11):

Note that often 0 - 1 is defined in Coq to be 0


Last updated: Jun 18 2024 at 20:02 UTC