mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-11-13 10:58:23 +03:00
Add some tests.
This commit is contained in:
parent
2f53602749
commit
9ecc8f720d
2
tests/modsys/T10.icry
Normal file
2
tests/modsys/T10.icry
Normal file
@ -0,0 +1,2 @@
|
||||
:module `T10::Main
|
||||
:browse `T10::Main
|
6
tests/modsys/T10.icry.stdout
Normal file
6
tests/modsys/T10.icry.stdout
Normal file
@ -0,0 +1,6 @@
|
||||
Loading module Cryptol
|
||||
Loading module T10::Main
|
||||
Symbols
|
||||
=======
|
||||
f : {T} T -> T
|
||||
|
9
tests/modsys/T10/Main.cry
Normal file
9
tests/modsys/T10/Main.cry
Normal file
@ -0,0 +1,9 @@
|
||||
module T10::Main where
|
||||
|
||||
parameter
|
||||
type T : *
|
||||
x : T
|
||||
|
||||
f : T
|
||||
f = x
|
||||
|
2
tests/modsys/T8.icry
Normal file
2
tests/modsys/T8.icry
Normal file
@ -0,0 +1,2 @@
|
||||
:module `T8::Main
|
||||
:t f
|
3
tests/modsys/T8.icry.stdout
Normal file
3
tests/modsys/T8.icry.stdout
Normal file
@ -0,0 +1,3 @@
|
||||
Loading module Cryptol
|
||||
Loading module T8::Main
|
||||
f : [8] -> [8]
|
8
tests/modsys/T8/Main.cry
Normal file
8
tests/modsys/T8/Main.cry
Normal file
@ -0,0 +1,8 @@
|
||||
module T8::Main where
|
||||
|
||||
parameter
|
||||
x : [8]
|
||||
|
||||
f : [8]
|
||||
f = x
|
||||
|
3
tests/modsys/T9.icry
Normal file
3
tests/modsys/T9.icry
Normal file
@ -0,0 +1,3 @@
|
||||
:module `T9::Main
|
||||
:t main
|
||||
main
|
5
tests/modsys/T9.icry.stdout
Normal file
5
tests/modsys/T9.icry.stdout
Normal file
@ -0,0 +1,5 @@
|
||||
Loading module Cryptol
|
||||
Loading module T9::A
|
||||
Loading module T9::Main
|
||||
main : [16]
|
||||
0x1010
|
10
tests/modsys/T9/A.cry
Normal file
10
tests/modsys/T9/A.cry
Normal file
@ -0,0 +1,10 @@
|
||||
module T9::A where
|
||||
|
||||
parameter
|
||||
type n : #
|
||||
type constraint fin n
|
||||
x : [n]
|
||||
|
||||
f : [n+n]
|
||||
f = x # x
|
||||
|
7
tests/modsys/T9/Main.cry
Normal file
7
tests/modsys/T9/Main.cry
Normal file
@ -0,0 +1,7 @@
|
||||
module T9::Main where
|
||||
|
||||
import `T9::A
|
||||
|
||||
main = f 0x10
|
||||
|
||||
|
Loading…
Reference in New Issue
Block a user