To focus the search input from anywhere on the page, press the 'S' key.
in-package search v0.1.0
Library
Module
Module type
Parameter
Class
Class type
Coq document type.
Pretty printing guidelines
Pp.t
is the main pretty printing document type in the Coq system. Documents are composed laying out boxes, and users can add arbitrary tag metadata that backends are free to interpret.
The datatype has a public view to allow serialization or advanced uses, however regular users are _strongly_ warned against its use, they should instead rely on the available functions below.
Box order and number is indeed an important factor. Try to create a proper amount of boxes. The ++
operator provides "efficient" concatenation, but using the list constructors is usually preferred.
That is to say, this:
hov [str "Term"; hov (pr_term t); str "is defined"]
is preferred to:
hov (str "Term" ++ hov (pr_term t) ++ str "is defined")
type doc_view =
| Ppcmd_empty
| Ppcmd_string of string
| Ppcmd_glue of t list
| Ppcmd_box of block_type * t
| Ppcmd_tag of pp_tag * t
| Ppcmd_print_break of int * int
| Ppcmd_force_newline
| Ppcmd_comment of string list
Formatting commands
val str : string -> t
val brk : (int * int) -> t
val fnl : unit -> t
val ws : int -> t
val mt : unit -> t
val ismt : t -> bool
val comment : string list -> t
Manipulation commands
Derived commands
val spc : unit -> t
val cut : unit -> t
val align : unit -> t
val int : int -> t
val real : float -> t
val bool : bool -> t
val qstring : string -> t
val qs : string -> t
val strbrk : string -> t
Boxing commands
Tagging
Printing combinators
val pr_comma : unit -> t
Well-spaced comma.
val pr_semicolon : unit -> t
Well-spaced semicolon.
val pr_bar : unit -> t
Well-spaced pipe bar.
val pr_spcbar : unit -> t
Pipe bar with space before and after.
Inner object preceded with a space if Some
, nothing otherwise.
val pr_nth : int -> t
Ordinal number with the correct suffix (i.e. "st", "nd", "th", etc.).
Concatenation of the list contents, without any separator.
Unlike all other functions below, prlist
works lazily. If a strict behavior is needed, use prlist_strict
instead.
prlist_with_sep sep pr [a ; ... ; c]
outputs pr a ++ sep () ++ ... ++ sep () ++ pr c
. where the thunk sep is memoized, rather than being called each place its result is used.
Indexed version of prvect_with_sep
.
pr_enum pr [a ; b ; ... ; c]
outputs pr a ++ str "," ++ spc () ++ pr b ++ str "," ++ spc () ++ ... ++ str "and" ++ spc () ++ pr c
.
pr_choice pr [a ; b ; ... ; c]
outputs pr a ++ str "," ++ spc () ++ pr b ++ str "," ++ spc () ++ ... ++ str "or" ++ spc () ++ pr c
.
Sequence of objects separated by space (unless an element is empty).
Main renderers, to formatter and to string
val pp_with : Format.formatter -> t -> unit
pp_with fmt pp
Print pp
to fmt
and don't flush fmt
val string_of_ppcmds : t -> string
val db_print_pp : Format.formatter -> t -> unit
Print the Pp in tree form for debugging
val db_string_of_pp : t -> string
Print the Pp in tree form for debugging, return as a string