WordMultiplication.multiply: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/word_multiplication.bend as WordMultiplication
Lines 134-136 of stelliferous@0.0.2.0/proofs/word_multiplication.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/word_multiplication.bend&start_line=134&end_line=136

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

def 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)}:
  %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)}
  multiply_go(n,n,a,Word.to_nat(n,b),0n)

Uses (10):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.mul
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.mul.go
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.to_nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.zero
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/word_arithmetic.bend&name=encode
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/word_multiplication.bend&name=multiply_go
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/word_multiplication.bend&name=word_roundtrip