diff options
| author | Chantal Keller <Chantal.Keller@lri.fr> | 2020-07-06 12:39:51 +0200 |
|---|---|---|
| committer | Chantal Keller <Chantal.Keller@lri.fr> | 2020-07-06 12:39:51 +0200 |
| commit | 6ddb77f5f60db1006c95552f893a71dd7571d966 (patch) | |
| tree | 757659a54179ad8bf7c9b702a73f354f5c0304c3 /src/BEST_PRACTICE.md | |
| parent | 6a0a78282219d1402457222d5728286836ab9f0f (diff) | |
| download | smtcoq-6ddb77f5f60db1006c95552f893a71dd7571d966.tar.gz smtcoq-6ddb77f5f60db1006c95552f893a71dd7571d966.zip | |
Clarify axiom usage (closes #71)
Diffstat (limited to 'src/BEST_PRACTICE.md')
| -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 |