When quick_and_dirty
mode is enabled, some regular proofs get replaced with skip proofs (i.e. sorry
oracles). For example, the following will throw an Exception when you build
it (curiously, the interactive session works just fine):
fun ex :: "'a ⇒ nat" where
"ex _ = 0"
theorem ex_const: "ex 5 = ex 7"
by auto
ML ‹
exception E;
if (Thm_Deps.has_skip_proof [@{thm ex_const}]) then raise E
else ()
›
Is there a reason for that? Or an option to disable this behavior?
Last updated: Jul 15 2022 at 23:21 UTC