def Inv

lawful-fields@0.1.1.0 · proof_num.bend:275

import Base

275# How num.go's (ok, acc) stands for dec.go's value m.
276def Inv(ok: Bool, +acc: U32, +m: Maybe<&2, Nat>, +M: Nat) -> Data:
277  match ok:
278    case True{}:
279      Sigma<&2, &2, {m == Some{U32.to_nat(acc)} : Maybe<&2, Nat>}, e => {Nat.is_lt(U32.to_nat(acc), M) == True{} : Bool}>
280    case False{}:
281      Bad(m, M)