def deadline_choose

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/lemmas/src/time.bend:18

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/types/model.bend as T
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/src/wide.bend as W

18def deadline_choose(now: T.Int64, ns: T.Int64, immortal: Bool) -> T.Int64:
19  match immortal:
20    case True{}:
21      T.I64{W.zero()}
22    case False{}:
23      add(now, milliseconds(ns))