From ad56f236ad65585da1d895b3754ad751bec1aade Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Sat, 5 Mar 2022 14:30:32 +0000 Subject: Remove the table of contents --- README.md | 9 --------- README.org | 1 + 2 files changed, 1 insertion(+), 9 deletions(-) diff --git a/README.md b/README.md index 5595e45..0d303cd 100644 --- a/README.md +++ b/README.md @@ -1,17 +1,8 @@ -- [BitEQ](#orged8a59e) - - [Difficulties of using Coq for bitvector proofs](#orga4f0f39) - - - - - # BitEQ Reasoning about bit equality for various rewrites. This is based on [proofs](resources/samc.lisp) done in ACL2, and uses the `bbv` library to convert the proofs into Coq. - - ## Difficulties of using Coq for bitvector proofs The main difficulty of using Coq for bitvector proofs is that the standard library is missing many proofs about numbers that have the form `x mod 2 ^ y`. These are crucial for bitvector arithmetic, but have to all be manually proven. One example of such a proof is the following Lemma. diff --git a/README.org b/README.org index 9730dd9..8d8e370 100644 --- a/README.org +++ b/README.org @@ -1,5 +1,6 @@ #+title: BitEQ #+author: Yann Herklotz +#+options: toc:nil * BitEQ -- cgit