format_WARNING : string -> string -> string -> string
STRUCTURE
Feedback
SYNOPSIS
Maps arguments of HOL_WARNING to a string.
DESCRIPTION
The format_WARNING function maps three strings to a string. Usually, the input strings are the arguments to an invocation of HOL_WARNING. format_WARNING is the default function used by WARNING_to_string.
FAILURE
Never fails.
EXAMPLE
- print (format_WARNING "Module" "function" "Gadzooks!");
<<HOL warning: Module.function: Gadzooks!>>

SEEALSO
Feedback, WARNING_to_string, format_ERR, format_MESG
HOL  Kananaskis-13