Can I in Coq define a recursive function with a notation such that the recursive calls can use it?

Question

Say I want to define add : nat -> nat -> nat with a notation Notation "a + b" := add a b and I want to write add as something like

Fixpoint add (a b : nat) : nat := match a with
| 0 => b
| S a => S (a + b) (* note the use of notation + *)

Where can I insert the notation definition so I can write the above?

This may look like an overkill for notation, but that's because it's a simplified example. The real use case is a very long definition, and I want to use notation to simplify it.

Answer 1

You can add a where clause at the end. See the documentation there:

https://coq.inria.fr/doc/V8.20.0/refman/user-extensions/syntax-extensions.html#grammar-token-decl_notations

Example:

Fixpoint plus (n m : nat) {struct n} : nat :=
match n with
    | O => m
    | S p => S (p + m)
end
where "n + m" := (plus n m).