diff options
| -rw-r--r-- | src/BEST_PRACTICE.md | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/src/BEST_PRACTICE.md b/src/BEST_PRACTICE.md index 783ef82..bbfd381 100644 --- a/src/BEST_PRACTICE.md +++ b/src/BEST_PRACTICE.md @@ -1,8 +1,12 @@ # Proofs ## Axioms -No axiom should be added. No library adding axioms should be imported -(except Int63 and Array). +No axiom should be added. No library adding axioms should be imported, +except: +- Int63 and Array, used in core SMTCoq +- ProofIrrelevance, to be used with care (it is currently used only to + treat equality over bit vectors and functional arrays, which are + implemented as dependent types). # Code organization |