GaloisInc/what4
1
1
Fork 0
mirror of https://github.com/GaloisInc/what4.git synced 2024-11-25 07:13:59 +03:00
Code Issues Projects Releases Wiki Activity

Remove getUnannotatedTerm case for bound variables

Browse Source
This commit is contained in:
Langston Barrett 2023-12-06 11:14:09 -05:00
parent be3e8b1189
commit e46dff4209
2 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
what4/src/What4/Expr/Builder.hs
View File

@ -1646,7 +1646,6 @@ instance IsExprBuilder (ExprBuilder t st fs) where
getUnannotatedTerm _sym e =
case e of
BoundVarExpr {} -> Just e
NonceAppExpr (nonceExprApp -> Annotation _ _ x) -> Just x
_ -> Nothing

3
what4/src/What4/Interface.hs
View File

@ -691,7 +691,8 @@ class ( IsExpr (SymExpr sym), HashableF (SymExpr sym), HashableF (BoundVar sym)
getAnnotation :: sym -> SymExpr sym tp -> Maybe (SymAnnotation sym tp)
-- | Project the original, unannotated term from an annotated term.
-- This returns 'Nothing' for terms that do not have annotations.
-- This returns 'Nothing' for terms that do not have annotations,
-- or for terms that cannot be separated from their annotations.
getUnannotatedTerm :: sym -> SymExpr sym tp -> Maybe (SymExpr sym tp)
----------------------------------------------------------------------