Open langston-barrett opened 11 months ago
This is a follow-up to #244, where we observed that BoundVarExprs already carry Nonces, so there's no need to create Annotation expressions for them. As it turns out, the same is true for {Nonce,}AppExpr:
BoundVarExpr
Nonce
Annotation
{Nonce,}AppExpr
https://github.com/GaloisInc/what4/blob/076f49b996bd328764a9c6edece6b7c34cb1cfb4/what4/src/What4/Expr/App.hs#L111
https://github.com/GaloisInc/what4/blob/076f49b996bd328764a9c6edece6b7c34cb1cfb4/what4/src/What4/Expr/App.hs#L125
Perhaps we should special-case these in the same way we did BoundVarExpr in #245.
This is a follow-up to #244, where we observed that
BoundVarExprs already carryNonces, so there's no need to createAnnotationexpressions for them. As it turns out, the same is true for{Nonce,}AppExpr:https://github.com/GaloisInc/what4/blob/076f49b996bd328764a9c6edece6b7c34cb1cfb4/what4/src/What4/Expr/App.hs#L111
https://github.com/GaloisInc/what4/blob/076f49b996bd328764a9c6edece6b7c34cb1cfb4/what4/src/What4/Expr/App.hs#L125
Perhaps we should special-case these in the same way we did
BoundVarExprin #245.