GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-08-17 09:50:35 +03:00
Code Issues Projects Releases Wiki Activity

Add a primitive for arrayEq

Browse Source 
Currently, this primitive (like the other Array primitives) has
no computational interpretation, and is only used for stating
specifications that are used in SAW. As such, there are no changes to
the interpreter.
This commit is contained in:
Robert Dockins 2022-07-20 09:43:41 -07:00
parent cfb16318b5
commit e66db956a8
1 changed files with 1 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
lib/Array.cry
View File

@ -10,6 +10,7 @@ primitive type Array : * -> * -> *
primitive arrayConstant : {a, b} b -> (Array a b)
primitive arrayLookup : {a, b} (Array a b) -> a -> b
primitive arrayUpdate : {a, b} (Array a b) -> a -> b -> (Array a b)
primitive arrayEq : {n, a} (Array [n] a) -> (Array [n] a) -> Bool
/**
* Copy elements from the source array to the destination array.