diff options
| author | Gereon Kremer <gkremer@stanford.edu> | 2020-12-18 08:59:43 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-12-18 08:59:43 +0100 |
| commit | 8a2a526b2dab5d6efaf1435afcc1b7be113a86bf (patch) | |
| tree | 135adecb0499c819ccec965721261a891be33396 /src/theory/arith/constraint.cpp | |
| parent | 0ae11d1abec9017784eefa2252d8e8ea7dfb4f74 (diff) | |
(proof-new) Add proof for tangent plane lemmas (#5700)
This PR adds a proof for the tangent plane lemmas from nl-ext.
As this lemma uses some insight about the tangent plane of a multiplication term, this PR adds a new proof rule.
Diffstat (limited to 'src/theory/arith/constraint.cpp')
0 files changed, 0 insertions, 0 deletions