Exception raised when an assertion fails. The arguments are the location of the assert keyword in the source code (file name, line number, column number).

Questa eccezione � per errori di corto-circuito che si ritirano direttamente al top level, evitando qualsiasi gestione per l'eccezioni di tipo HolFail.

Essa consiste di una stringa (per convenzione in maiuscolo) che classifica l'eccezione i in modo generico, e di un messaggio che descrive l'eccezione in qualche dettaglio.

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

Questa eccezzione � per semplici flussi di controllo locali, sollevata per uscire dalla parte principale di una funzione e tipicamente gestita da un try-catch pi� esterno della stessa funzione.

Questa pu� essere utile per rimuovere segnalazioni disordinate di errore dal corpo principale di una funzione e raggrupparle insieme alla fine. E' anche usata come ultima spiaggia in flussi di controllo senza errori,

quando non c'� nulla di pi� elegante.