Skip to content

Commit

Permalink
Add regression test for issue #485.
Browse files Browse the repository at this point in the history
  • Loading branch information
Brian Huffman committed Sep 23, 2020
1 parent 24f21fb commit d7104a5
Show file tree
Hide file tree
Showing 4 changed files with 31 additions and 0 deletions.
4 changes: 4 additions & 0 deletions tests/issues/issue485.icry
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
:l issue485b.cry
:t foo
:t bar
:t baz
8 changes: 8 additions & 0 deletions tests/issues/issue485.icry.stdout
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
Loading module Cryptol
Loading module Cryptol
Loading module Float
Loading module issue485a
Loading module issue485b
foo : [3]
bar : [8] -> [8]
baz : [8] -> [8] -> [8]
16 changes: 16 additions & 0 deletions tests/issues/issue485a.cry
Original file line number Diff line number Diff line change
@@ -0,0 +1,16 @@
module issue485a where

import Float

private type A = [8] -> [8]

private type ByteFun t = [8] -> t

foo : RoundingMode
foo = 0

bar : A
bar x = x

baz : ByteFun (ByteFun [8])
baz = (+)
3 changes: 3 additions & 0 deletions tests/issues/issue485b.cry
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
module issue485b where

import issue485a

0 comments on commit d7104a5

Please sign in to comment.