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: Jun 18 2024 at 22:01 UTC