[@inline:trivial] on the definition of a predicate is useful because it allows proofs to directly use the definition of the predicate. But it seems to also make it hard to prove that a use of a predicate follows from itself. Eg if pred has this annotation, then having
pred a b c d as a hypothesis does not make it easy to prove pred a b c d as a goal. Would it make sense to have [@inline:trivial] keep two copies of pred a b c d as hypotheses, one inlined and one not? thanks, julia _______________________________________________ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
