def multiply

stelliferous@0.0.2.0 · proofs/word_multiplication.bend:134

import Base
import stelliferous@0.0.2.0/proofs/word_arithmetic.bend as WordArithmetic

134def multiply(+n: Nat,+a: Word(n),+b: Word(n)) -> {Word.mul(n,a,b) == WordArithmetic.encode(Nat.mul(Word.to_nat(n,a),Word.to_nat(n,b)),n) : Word(n)}:
135  %word_roundtrip(n,b) : {Word.mul.go(n,n,a,_,Word.zero(n)) == WordArithmetic.encode(Nat.mul(Word.to_nat(n,a),Word.to_nat(n,b)),n) : Word(n)}
136  multiply_go(n,n,a,Word.to_nat(n,b),0n)