def add

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/lemmas/spec/numeric.bend:51

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/types/model.bend as T

51def add(a: T.Int64, b: T.Int64) -> T.Int64:
52  match a b:
53    case T.I64{x} T.I64{y}:
54      T.I64{from_nat(64n, Nat.add(unsigned(64n, x), unsigned(64n, y)))}