cryptol/tests/mono-binds/test01.icry.stdout

32 lines
830 B
Plaintext
Raw Normal View History

Loading module Cryptol
Loading module Cryptol
Loading module test01
module test01
import Cryptol
/* Not recursive */
test01::a : {n, a} (fin n) => [n]a -> [2 * n]a
test01::a = \{n, a} (fin n) (x : [n]a) ->
test01::f n x
2017-02-09 04:24:15 +03:00
where
/* Not recursive */
test01::f : {m} [m]a -> [n + m]a
test01::f = \{m} (y : [m]a) -> (Cryptol::#) n m a <> x y
2017-02-09 04:24:15 +03:00
Loading module Cryptol
Loading module test01
module test01
import Cryptol
/* Not recursive */
test01::a : {n, a} (fin n) => [n]a -> [2 * n]a
test01::a = \{n, a} (fin n) (x : [n]a) ->
2017-02-09 04:24:15 +03:00
test01::f x
where
/* Not recursive */
test01::f : [n]a -> [2 * n]a
test01::f = \ (y : [n]a) -> (Cryptol::#) n n a <> x y
2017-02-09 04:24:15 +03:00