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?

Fabian Huch (Feb 21 2022 at 14:07):

Apparently quick_and_dirty also axiomatizes some datatype/function constructions (so that they are faster), which is the reason the above fails. Except for locally disabling quick_and_dirty, there does not seem to be an option to turn that off.

Notification Bot (Feb 21 2022 at 14:07):

Fabian Huch has marked this topic as resolved.

Last updated: Dec 21 2024 at 12:33 UTC