Skip to content

Commit 634b928

Browse files
committed
copilot: Update example to demonstrate struct update support. Refs #524.
This commit updates the `what4-structs` example in `copilot` (which depends on `copilot-theorem`) in order to demonstrate that `copilot-theorem` supports reasoning about a basic theorem involving a struct field update.
1 parent d939de5 commit 634b928

File tree

1 file changed

+4
-0
lines changed

1 file changed

+4
-0
lines changed

copilot/examples/what4/Structs.hs

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -64,6 +64,10 @@ spec = do
6464
void $ prop "Example 2" $ forAll $
6565
(((battery#other) .!! 2) .!! 3) == (((battery#other) .!! 2) .!! 4)
6666

67+
-- Update a struct field, then check it for equality.
68+
void $ prop "Example 3" $ forAll $
69+
((battery ## temp =$ (+1))#temp == (battery#temp + 1))
70+
6771
main :: IO ()
6872
main = do
6973
spec' <- reify spec

0 commit comments

Comments
 (0)