Questa eccezione � per errori che possono raggiungere alla fine il top level, ma che possono anche essere trappate chiamando delle funzioni. E' l'eccezione classica per casi di errore nelle funzioni di HOL Zero.
Consiste del nome della funzione che fallisce e di un messaggio che descrive l'errore con qualche dettaglio. Di sotto sono definite varie funzioni per sollevare e trappare gli HolFails| Record Field | Description |
Full Usage:
Data0
Field type: string * string
|
|