Re: [isabelle] type-unsound error
Il ven 4 ott 2013 10:53 CEST, Jasmin Blanchette ha scritto:
>A few years ago, as Sledgehammer's translation code was evolving rapidly, this message usually indicated a bug in Sledgehammer. These days, the last N times that people have reported this error to me, it was because of a "sorry" that turned out to be unprovable.
...and this turned out to be the case, too. Sorry about my unprovable sorries.
>Incidentally, the message in Isabelle2013-1-RC should be slightly more helpful:
> The prover derived "False" using foo, bar, and baz.
> This could be due to inconsistent axioms (including "sorry"s)
> or to a bug in Sledgehammer. If the problem persists, please
> contact the Isabelle developers.
Definitely more helpful. This thread, too, could be of future reference.
This archive was generated by a fusion of
Pipermail (Mailman edition) and