mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-09-11 22:17:18 +03:00
Update old cryptol-1 syntax in example code.
This commit is contained in:
parent
030349f6de
commit
7da982ab2d
@ -33,8 +33,8 @@ call {\tt riffle} with a sequence that has an odd number of elements?
|
|||||||
|
|
||||||
\begin{Answer}\ansref{ex:misc:riffle}
|
\begin{Answer}\ansref{ex:misc:riffle}
|
||||||
\begin{code}
|
\begin{code}
|
||||||
riffle xs = join [| [x y] || x <- fh || y <- sh |]
|
riffle xs = join [ [x, y] | x <- fh | y <- sh ]
|
||||||
where [fh sh] = split xs;
|
where [fh, sh] = split xs
|
||||||
\end{code}
|
\end{code}
|
||||||
The Cryptol type-checker will {\em not} allow passing an odd number of
|
The Cryptol type-checker will {\em not} allow passing an odd number of
|
||||||
elements to {\tt riffle}. To see the error message, issue: {\tt riffle
|
elements to {\tt riffle}. To see the error message, issue: {\tt riffle
|
||||||
@ -50,8 +50,8 @@ elements to {\tt riffle}. To see the error message, issue: {\tt riffle
|
|||||||
we will just use 8-bit numbers.
|
we will just use 8-bit numbers.
|
||||||
\begin{code}
|
\begin{code}
|
||||||
riffle8 : [52][8] -> Bit;
|
riffle8 : [52][8] -> Bit;
|
||||||
theorem riffle8: {deck}. decks @ 8 == deck
|
property riffle8 deck = decks @ 8 == deck
|
||||||
where decks = [deck] # [| riffle d || d <- decks |];
|
where decks = [deck] # [ riffle d | d <- decks ]
|
||||||
\end{code}
|
\end{code}
|
||||||
\end{Answer}
|
\end{Answer}
|
||||||
|
|
||||||
|
Loading…
Reference in New Issue
Block a user