`Need` second argument can rely on first being false about libraries HOT 1 OPEN

include "Wrappers.dfy"

module MoreWrappers {

  import opened Wrappers

  function method LazyNeed<E>(condition: bool, errorThunk: () --> E): (result: Outcome<E>)
    requires !condition ==> errorThunk.requires()
  {
    if condition then Pass else Fail(errorThunk())
  }

  function Work() : Result<int, string> {
    var something := Magic();
    :- LazyNeed(|something| == 0, () requires |something| > 0 => "Woops => " + Join(something, ","));
    Success(42)
  }

  function Magic(): seq<string>

  function Join(ss: seq<string>, sep: string) : string
    requires 0 < |ss|
}