In trying to do math with both N and nat types at the same time, and I wondered if there was a better way to handle multiple different numeric type notations at the same time. Even just providing the constant zero value collides between these two types.

I still have N_scope open, but because I open nat_scope just for this one definition, it seems to have priority if a notation is used by both nat and N.

I'm solving an Advent of Code problem from 2017 to get some practice in: "Now, instead of considering the next digit, it wants you to consider the digit halfway around the circular list. That is, if your list contains 10 items, only include a digit in your sum if the digit 10/2 = 5 steps forward matches it. Fortunately, your list has an even number of elements."

```
Definition matchHalfway (lv : list N) (index : nat) :=
let len := length lv in
let target := (index + (len / 2)) mod len in
let o := nth index lv N.zero in
let m := nth target lv N.zero in
if N.eqb o m then o else N.zero.
```

Also, is there an array type that would better for indexing than lists? I know linked lists are particularly awful at this.

I guess, assuming the proper require imports, `42%N`

should be the constant of type N whereas `42%nat`

should be of type nat? Then you can `Local Open Scope N_scope`

in your file if have more of the former.

Pierre Roux said:

I guess, assuming the proper require imports,

`42%N`

should be the constant of type N whereas`42%nat`

should be of type nat? Then you can`Local Open Scope N_scope`

in your file if have more of the former.

Yeah I just changed N.zero to 0%N. But I still have equality in N and addition in nat. It's not that bad in a toy example I guess.

I'm using N for the list values because I'm converting from ascii input to numeric, and that used N.

You can similarly do `(x + y)%N`

and `(x + y)%nat`

(see the refman page https://coq.inria.fr/doc/V8.18.0/refman/user-extensions/syntax-extensions.html for (a lot of) details about notatins).

ah ok, that's helpful.

also, there seems to be no boolean comparison on N, is that the case. I just used

```
match N.compare n 48 with
| Lt => 0
| _ => n - 48
```

instead.

There is `N.eqb`

, notation `(x =? y)%N`

.

I see it now. Thanks for your help!

Last updated: Jun 22 2024 at 16:02 UTC