HOL icon indicating copy to clipboard operation
HOL copied to clipboard

Pattern-matching compilation fails

Open mn200 opened this issue 4 years ago • 1 comments

With the "classic" heuristic, this works. Now, with the new default, it fails (with an exception about missing cases):

val foo_def = Define`
    (foo 0 0 0 = 0) /\ (foo 0 0 1 = 1) /\ (foo 0 1 0 = 1) /\ (foo 0 1 1 = 0) /\
    (foo 1 0 0 = 0) /\ (foo 1 0 1 = 1) /\ (foo 1 1 0 = 0) /\ (foo 1 1 1 = 0)`;

Thanks to Joseph Chan for the bug report.

mn200 avatar Jun 16 '20 05:06 mn200

The exception is raised by Defn.stdrec_defn

mn200 avatar Mar 07 '22 02:03 mn200