It’s important to understand that blast knows nothing about type classes. This isn’t a problem for rules like order_trans, where the type class constraint would be satisfied in most cases. But it’s fatal for continuous_on_discrete: it will succeed in all cases, but if the type class constraint isn’t satisfied (and it usually won’t be), then the proof will fail and it’s not clear that backtracking will find an alternative. The PROOF FAILED message (if it still exists) alerts us to this.
Larry > On 1 Sep 2018, at 13:39, Manuel Eberl <ebe...@in.tum.de> wrote: > >> This thread consists of two sub-threads. The hardware / OS question >> still needs to be sorted out: it might be something with Arch Linux. > > I don't really have much of an opportunity to test this on other systems > atm, but I'll see what I can do. > >> Apart from that, my reading of blast.ML is that the "continuous_on" rule >> is applied in the search independently of its fine-grained type >> information. Is that correct? > > Even if it is, it has no preconditions, so I don't see how it could > cause nontermination. > > Manuel _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
