diff options
| author | Alex Ozdemir <aozdemir@hmc.edu> | 2020-01-31 23:44:24 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-01-31 23:44:24 -0800 |
| commit | 7583e034bbd991877b634d50249bbccfd9e3c763 (patch) | |
| tree | 9c4034b7eaa5a10663347f945dfb3362bcd913e9 /contrib | |
| parent | c099abeb9c3a45019b18daac19c4b4cd43b4c6f0 (diff) | |
Handle `expectedType` in TheoryProofEngine (#3691)
`TheoryProofEngine` now uses the `expectedType` optional argument.
* When printing terms, it sets this for theories that it dispatches too
* It occasionally asks theories for help determining the `expectedType` using `equalityType`, which has a sensible default implementation.
* It is mindful of `expectedType` when using the let map.
I also moved to hpp function implementations into the cpp.
Diffstat (limited to 'contrib')
0 files changed, 0 insertions, 0 deletions