Commit a2d2bb7b authored by Heiko Becker's avatar Heiko Becker
Browse files

Fix small bug

parent f480aff7
......@@ -40,7 +40,7 @@ Definition isSoundErrBin (op:binop) (e1:exp R) (val_e1:ann) (e2:exp R) (val_e2:a
=> isSupersetInterval (getIntv val) (addInterval (getIntv val_e1) (getIntv val_e2)) /\
isSoundErr (getErr val) (getIntv val) (getErr val_e1 + getErr val_e2)%R
|Sub
=> isSupersetInterval (getIntv val) (substractInterval (getIntv val_e1) (getIntv val_e2)) /\
=> isSupersetInterval (getIntv val) (subtractInterval (getIntv val_e1) (getIntv val_e2)) /\
isSoundErr (getErr val) (getIntv val) (getErr val_e1 - getErr val_e2)%R
|Mult
=> isSupersetInterval (getIntv val) (multInterval (getIntv val_e1) (getIntv val_e2)) /\
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment