mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-11-28 01:13:34 +03:00
87 lines
3.1 KiB
Plaintext
87 lines
3.1 KiB
Plaintext
Loading module Cryptol
|
|
Loading module Cryptol
|
|
Loading module test05
|
|
[warning] at ./test05.cry:9:3--9:6
|
|
This binding for foo shadows the existing binding from
|
|
(at ./test05.cry:4:1--4:4, foo)
|
|
[warning] at ./test05.cry:13:5--13:8
|
|
This binding for foo shadows the existing binding from
|
|
(at ./test05.cry:9:3--9:6, foo)
|
|
module test05
|
|
import Cryptol
|
|
/* Not recursive */
|
|
test05::foo : [10]
|
|
test05::foo = Cryptol::demote 10 10 <> <> <>
|
|
|
|
/* Not recursive */
|
|
test05::test : {a, b, c} (Zero b, c >= 4, fin c) => [a]b -> [c]
|
|
test05::test = \{a, b, c} (Zero b, c >= 4, fin c) (a : [a]b) ->
|
|
Cryptol::demote 10 c <> <> <>
|
|
where
|
|
/* Not recursive */
|
|
test05::foo : [10]
|
|
test05::foo = Cryptol::demote 10 10 <> <> <>
|
|
|
|
/* Not recursive */
|
|
test05::f : {d} (fin d) => [a + d]b
|
|
test05::f = \{d} (fin d) ->
|
|
test05::bar d <>
|
|
where
|
|
/* Not recursive */
|
|
test05::foo : [a]b
|
|
test05::foo = a
|
|
|
|
/* Not recursive */
|
|
test05::bar : {e} (fin e) => [e + a]b
|
|
test05::bar = \{e} (fin e) ->
|
|
(Cryptol::#) e a b <> (Cryptol::zero ([e]b) <>) test05::foo
|
|
|
|
|
|
|
|
|
|
|
|
Loading module Cryptol
|
|
Loading module test05
|
|
[warning] at ./test05.cry:9:3--9:6
|
|
This binding for foo shadows the existing binding from
|
|
(at ./test05.cry:4:1--4:4, foo)
|
|
[warning] at ./test05.cry:13:5--13:8
|
|
This binding for foo shadows the existing binding from
|
|
(at ./test05.cry:9:3--9:6, foo)
|
|
[warning] at ./test05.cry:1:1--14:21:
|
|
Defaulting 1st type parameter
|
|
of expression (#)
|
|
at ./test05.cry:14:11--14:21
|
|
to 0
|
|
module test05
|
|
import Cryptol
|
|
/* Not recursive */
|
|
test05::foo : [10]
|
|
test05::foo = Cryptol::demote 10 10 <> <> <>
|
|
|
|
/* Not recursive */
|
|
test05::test : {a, b, c} (Zero b, c >= 4, fin c) => [a]b -> [c]
|
|
test05::test = \{a, b, c} (Zero b, c >= 4, fin c) (a : [a]b) ->
|
|
Cryptol::demote 10 c <> <> <>
|
|
where
|
|
/* Not recursive */
|
|
test05::foo : [10]
|
|
test05::foo = Cryptol::demote 10 10 <> <> <>
|
|
|
|
/* Not recursive */
|
|
test05::f : [a]b
|
|
test05::f = test05::bar
|
|
where
|
|
/* Not recursive */
|
|
test05::foo : [a]b
|
|
test05::foo = a
|
|
|
|
/* Not recursive */
|
|
test05::bar : [a]b
|
|
test05::bar = (Cryptol::#) 0 a b <> (Cryptol::zero ([0]b) <>) test05::foo
|
|
|
|
|
|
|
|
|
|
|