GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-10-04 01:17:40 +03:00
Code Issues Projects Releases Wiki Activity

Use Integer in head and last.

Browse Source 
This is a bit of an overkill, as clearly 0 doesn't need it,
but it ensures maximum compatibility with the old behavior.
This commit is contained in:
Iavor Diatchki 2024-06-02 00:04:53 -07:00
parent d599934038
commit 4f2cf7d5fa
1 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
lib/Cryptol.cry
View File

@ -850,13 +850,13 @@ tail xs = drop`{1} xs
* Return the first (left-most) element of a sequence.
*/
head : {n, a} [1 + n]a -> a
head xs = xs @ (0 : [64])
head xs = xs @ (0 : Integer)
/**
* Return the right-most element of a sequence.
*/
last : {n, a} (fin n) => [1 + n]a -> a
last xs = xs ! (0 : [64])
last xs = xs ! (0 : Integer)
/**
* Same as 'split', but with a different type argument order.