|
(* Title: HOL/Mirabelle/Tools/mirabelle_arith.ML
Author: Jasmin Blanchette and Sascha Boehme, TU Munich
*)
structure Mirabelle_Arith : MIRABELLE_ACTION =
struct
fun arith_tag id = "#" ^ string_of_int id ^ " arith: "
fun init _ = I
fun done _ _ = ()
fun run id ({pre, timeout, log, ...}: Mirabelle.run_args) =
if Mirabelle.can_apply timeout Arith_Data.arith_tac pre
then log (arith_tag id ^ "succeeded")
else ()
handle Timeout.TIMEOUT _ => log (arith_tag id ^ "timeout")
fun invoke _ = Mirabelle.register (init, Mirabelle.catch arith_tag run, done)
end
¤ Dauer der Verarbeitung: 0.2 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
