Stream: Coq users

Topic: matching of nat


view this post on Zulip pianke (May 27 2022 at 01:19):

I am calling a function recursively n time. Is it possible to stop the function early at some value r(nat) ? How i should write it? Now match both n and r?

view this post on Zulip Li-yao (May 27 2022 at 03:30):

match Nat.eqb n r


Last updated: Jan 27 2023 at 01:03 UTC