ProofNum.Inv: def of lawful-fields@0.1.1.0
Import: import lawful-fields@0.1.1.0/proof_num.bend as ProofNum
Lines 275-281 of lawful-fields@0.1.1.0/proof_num.bend: https://jend.leeeet.dev/read.txt?path=lawful-fields@0.1.1.0/proof_num.bend&start_line=275&end_line=281

import Base

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

Uses (8):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat
  https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/proof_num.bend&name=Bad