diff options
| -rw-r--r-- | test/srg/srg0001/test.gf | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/test/srg/srg0001/test.gf b/test/srg/srg0001/test.gf new file mode 100644 index 000000000..6671918ec --- /dev/null +++ b/test/srg/srg0001/test.gf @@ -0,0 +1,4 @@ +cat S; +fun f : S; + +lin f = { s = variants {"a"; "b"} ++ variants {"c"; "d"} ++ variants {"e"; "f"} ++ variants { "g";"h";} } ;
\ No newline at end of file |