Number Notation dans Coq (démonstration)

L'assistant de preuve Coq dispose d'une fonctionnalité permettant à l'utilisateur de dénir ses propres notations avec une grande souplesse. Dans ce cadre, les constantes numériques étaient initialement interprétées et achées par du code dédié dans des plugins OCaml. Depuis Coq 8.9 (janvier 2019), la commande Numeral Notation (aujourd'hui renommée Number Notation) permet d'implémenter ces parsers et printers de constantes numériques directement dans Coq. Suite entre autre à l'introduction des ottants primitifs, cette commande a depuis connue un certain nombre d'extensions qui seront présentées dans cette démonstration : valeurs à virgules ou exposant, valeurs hexadécimales, interprétation vers des types inductifs paramétrés ou non inductifs.