## Stream: Coq users

### Topic: Working with multiple numeric types with notations

#### Anthony Peterson (Nov 02 2023 at 13:05):

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.

#### Pierre Roux (Nov 02 2023 at 13:08):

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.

#### Anthony Peterson (Nov 02 2023 at 13:09):

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.

#### Anthony Peterson (Nov 02 2023 at 13:10):

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

#### Pierre Roux (Nov 02 2023 at 13:14):

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).

#### Anthony Peterson (Nov 02 2023 at 13:17):

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
``````

There is `N.eqb`, notation `(x =? y)%N`.