Simpadd0-expr
Transform an expression.
- Signature
(simpadd0-expr expr gin state) → (mv new-expr gout)
- Arguments
- expr — Guard (exprp expr).
- gin — Guard (simpadd0-ginp gin).
- Returns
- new-expr — Type (exprp new-expr).
- gout — Type (simpadd0-goutp gout).
When we encounter an expression x + 0 that we transform into x,
we also generate a theorem saying that
executing the two expressions give equivalent results.
This is proved by essentially just instantiating
simpadd0-supporting-lemma
(see its documentation, also in regard to the exact way in which
we express the equivalence).
This is a very preliminary theorem generation capability,
which we plan to extend soon.
