Rainbow documentation

Rainbow is an open-source theorem prover written in Clojure. A small kernel checks every proof, and proofs are ordinary Clojure data. These pages document the open core, version 1.5.5. The code is on GitHub under Apache-2.0.

Every proof and lemma in the open core

theorems

4,030

definitions

1,205

modules

1,196

• The Applied Higher-Order Functions catalogue 322
• Signed rationals 147
• Non-negative rationals 140
• Finite types, distributions and Markov chains 122
• Lemmas behind operations-research checks 104
• Matrices 100
• Algorithm guarantees 85
• Vectors 44
• Finite sums 37
• Natural numbers 29
• Sets 16
• Logic 16
• Graph algorithms 8
• Foundations 8
• Analysis 6
• Finite sets 5
• Rationals 4
• Binary numerals 2
• Data types 1

Browse the reference