Stream: General

Topic: `quick_and_dirty` mode skips regular proofs

Fabian Huch (Feb 17 2022 at 12:33):

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