Mentions légales du service

Skip to content
  • Andrei Paskevich's avatar
    Vc: no more "liberal_for" · fb77f394
    Andrei Paskevich authored
    Instead, we put a "stop_split" over the subsequent postcondition
    under the (begin > end + 1) assumption. When this assumption is
    unrealizable (strict for), this allows us to discharge the whole
    branch as a single goal.
    fb77f394