vaishnavi08

Make command fails with Coq 8.11.1

2

Make fails when run with Coq 8.11.1. The output is as follows: `$make` ``` Generating Makefile make -f Makefile.coq.all make[1]: Entering directory '/home/vaishnavi/kami' COQDEP VFILES COQC Kami/Lib/StringStringAsOT.v File "./Kami/Lib/StringStringAsOT.v", line...

Multiplier correctness example

1

Hi, I'm new to coq and I am facing a few issues with understanding the code `MultiplierCorrectness.v`. I could understand till the lemma `mul_to_partial_mul`. I don't understand what the rest...