def Bad

lawful-fields@0.1.1.0 · proof_num.bend:267

import Base

267# The value dec has so far can no longer give a number below M.
268def Bad(m: Maybe<&2, Nat>, +M: Nat) -> Data:
269  match m:
270    case None{}:
271      Unit
272    case Some{v}:
273      {Nat.is_lt(v, M) == False{} : Bool}