failwith
Feedback.failwith : string -> 'a
Raise a HOL_ERR.
The function failwith raises a HOL_ERR with default values. This is
useful when detailed error tracking is not necessary.
failwith differs from fail in that it takes an extra string
argument, which is typically used to tell which function failwith is
being called from.
Failure
Always fails.
Example
> failwith "foo" handle e => Raise e;
Exception- The type of (it) contains a free type variable. Setting it to a unique
monotype.
HOL_ERR (at ??.failwith: foo) raised