law push_and

lawful-fields@0.1.1.0 · proof_digits.bend:55

import Base
import lawful-fields@0.1.1.0/defs.bend as F

55law push_and:
56  for +m: Maybe<&2, Nat>
57  for +x: U32
58  for +r: Bool
59  {Bool.and(Maybe.is_some(&2, Nat, F.dec.push(m, F.digit(x))), r) == Bool.and(Bool.and(Maybe.is_some(&2, Nat, m), Bool.and(U32.is_ge(x, 48), U32.is_le(x, 57))), r) : Bool}