mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-12-18 13:31:50 +03:00
32 lines
828 B
Plaintext
32 lines
828 B
Plaintext
|
Loading module Cryptol
|
||
|
|
Loading module Cryptol
|
||
|
|
Loading module test03
|
||
|
|
module test03
|
||
|
|
import Cryptol
|
||
|
|
/* Not recursive */
|
||
|
|
test03::test : {a} (fin a, a >= width a) => [a]
|
||
|
|
test03::test = \{a} (fin a, a >= width a) ->
|
||
|
|
foo a <> <>
|
||
|
|
where
|
||
|
|
/* Not recursive */
|
||
|
|
foo : {b} (fin b, b >= width a) => [b]
|
||
|
|
foo = \{b} (fin b, b >= width a) -> demote a b <> <> <>
|
||
|
|
|
||
|
|
|
||
|
|
|
||
|
|
Loading module Cryptol
|
||
|
|
Loading module test03
|
||
|
|
module test03
|
||
|
|
import Cryptol
|
||
|
|
/* Not recursive */
|
||
|
|
test03::test : {a} (fin a, a >= width a) => [a]
|
||
|
|
test03::test = \{a} (fin a, a >= width a) ->
|
||
|
|
foo
|
||
|
|
where
|
||
|
|
/* Not recursive */
|
||
|
|
foo : [a]
|
||
|
|
foo = demote a a <> <> <>
|
||
|
|
|
||
|
|
|
||
|
|
|