CODEWITHSUNDEEP
coq
user1494846
user1494846

Reputation: 244

Trouble writing my notation for natural numbers in Coq

Why does Coq not accept this?

Notation "[ d1 , .. , d2 ]" := (addition (multiply ( .. d1 .. ) ten) d2).

Upvotes: 1

Views: 251

Answers (1)

Gilles 'SO- stop being evil'
Gilles 'SO- stop being evil'

Reputation: 107759

Recursive notations need to obey fairly strict rules. The pattern to repeat must appear twice (that's how Coq knows what is to be repeated): once using d2 around the hole, and once using d1 around a terminating expression. You've only used your pattern once, using d2 around the hole. You need another iteration, around some zero (like nil in the notation for lists).

Notation "[ d1 , .. , d2 ]" :=
  (addition (multiply .. (addition (multiply zero ten) d1) .. ten) d2).

If you don't wish to introduce a zero, you can require at least two digits inside the brackets (instead of just one as above), and use that as the terminating expression. This is like the notation for pairs (in Init/Notations.v, also presented in the manual). You could complement this with a notation for [d0] with lower priority, but as this is just d0 there isn't much point.

Notation "[ d0 , d1 , .. , d2 ]" :=
  (addition (multiply .. (addition (multiply d0 ten) d1) .. ten) d2).

Upvotes: 2

Related Questions