GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-12-18 05:21:57 +03:00
Code Issues Projects Releases Wiki Activity

Add a test for record updating.

Browse Source 
This completes the implementation of record updates.
Fixes #399
This commit is contained in:
Iavor Diatchki 2020-01-21 11:35:19 -08:00
parent 38471c0cbc
commit 3038eacf54
3 changed files with 18 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
tests/regression/rec-update.cry Normal file
View File

@ -0,0 +1,8 @@
type T = { x : [8], y : Bool }
f1 = { x = 2, y = True } : T
f2 = { f1 | x = 3 }
f3 = { f2 | x = 4, y = False }
f4 = { f3 | x -> x + 1 }
f5 = [f1,f2,f3,f4]
f6 = { f5 | x = [7,8,9,10] }

3
tests/regression/rec-update.icry Normal file
View File

@ -0,0 +1,3 @@
:load rec-update.cry
f5
f6

7
tests/regression/rec-update.icry.stdout Normal file
View File

@ -0,0 +1,7 @@
Loading module Cryptol
Loading module Cryptol
Loading module Main
[{x = 0x02, y = True}, {x = 0x03, y = True}, {x = 0x04, y = False},
{x = 0x05, y = False}]
[{x = 0x07, y = True}, {x = 0x08, y = True}, {x = 0x09, y = False},
{x = 0x0a, y = False}]