Library Ltac2.Printf


Require Import Ltac2.Message.

This file defines a printf notation for easiness of writing messages
The built-in "format" notation scope can be used to create well-typed variadic printing commands following a printf-like syntax. The "format" scope parses quoted strings which contain either raw string data or printing specifications. Raw strings will be output verbatim as if they were passed to Ltac2.Message.of_string.
Printing specifications are of the form
'%' type
where the type value defines which kind of arguments will be accepted and how they will be printed. They can take the following values.
TODO: add printing modifiers.

Ltac2 printf fmt := Format.kfprintf print fmt.
Ltac2 fprintf fmt := Format.kfprintf (fun x => x) fmt.

The two following notations are made available when this module is imported.

Ltac2 Notation "printf" fmt(format) := printf fmt.
Ltac2 Notation "fprintf" fmt(format) := fprintf fmt.