~/jendhub

def multiply_zero_left

stelliferous@0.0.2.0 · proofs/bounded_u32_arithmetic.bend:48

import stelliferous@0.0.2.0/proofs/bounded_u32_arithmetic.bend as BoundedU32Arithmetic
import Base
import stelliferous@0.0.2.0/proofs/word_multiplication.bend as Multiplication

48def multiply_zero_left(+value: U32) -> {(0 * value : U32) == 0 : U32}:
49  Multiplication.native_multiply(0,value)

Uses (3)

Used by (0)

No other definition uses this definition.