/* Generated by F* Custard extraction. Do not edit. */
#include "Multiply.h"

void Multiply_multiply(uint32_t *x, uint32_t *y) {
  uint32_t n = x[0];
  uint32_t m = y[0];
  x[0] = 0;
  uint32_t ctr = 0;
  while (ctr < m) {
    uint32_t __anf0 = x[0];
    x[0] = (__anf0 + n);
    uint32_t __anf01 = ctr;
    ctr = (__anf01 + 1);
  }
}