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.
-
i
: takes an argument of type int and behaves as Message.of_int
-
I
: takes an argument of type ident and behaves as Message.of_ident
-
s
: takes an argument of type string and behaves as Message.of_string
-
t
: takes an argument of type constr and behaves as Message.of_constr
-
a
: takes two arguments f
of type (unit -> 'a -> message)
and x
of type 'a
and behaves as f () x
-
%
: outputs %
verbatim
TODO: add printing modifiers.