aboutsummaryrefslogtreecommitdiffstats
path: root/README.org
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2022-03-03 18:10:39 +0000
committerYann Herklotz <git@yannherklotz.com>2022-03-03 18:10:53 +0000
commitf7401188640f8f6726b933e0421400419b62c9b2 (patch)
treef88413843c2d36c0c9ae200f7efae047ee0116db /README.org
parentd84ee165a8f403792e0d613932763509d0f0480b (diff)
downloadbiteq-f7401188640f8f6726b933e0421400419b62c9b2.tar.gz
biteq-f7401188640f8f6726b933e0421400419b62c9b2.zip
Add README and markdown README
Diffstat (limited to 'README.org')
-rw-r--r--README.org3
1 files changed, 2 insertions, 1 deletions
diff --git a/README.org b/README.org
index 702319a..cba18aa 100644
--- a/README.org
+++ b/README.org
@@ -1,4 +1,5 @@
#+title: BitEQ
#+author: Yann Herklotz
-Reasoning about bit equality
+Reasoning about bit equality for various rewrites. This is based on [[file:resources/samc.lisp][proofs]] done in ACL2, and uses
+the =bbv= library to convert the proofs into Coq.