law push_some

lawful-fields@0.1.1.0 · proof_digits.bend:42

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

42law push_some:
43  for +a: Nat
44  for +x: U32
45  for +b: Bool
46  {Maybe.is_some(&2, Nat, F.dec.push(Some{a}, F.digit.if(x, b))) == b : Bool}