mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2024-11-28 05:32:03 +03:00
Add test of noNewtype
This commit is contained in:
parent
84e431f495
commit
69aff544b6
@ -98,7 +98,7 @@ chezTests : List String
|
|||||||
chezTests
|
chezTests
|
||||||
= ["chez001", "chez002", "chez003", "chez004", "chez005", "chez006",
|
= ["chez001", "chez002", "chez003", "chez004", "chez005", "chez006",
|
||||||
"chez007", "chez008", "chez009", "chez010", "chez011", "chez012",
|
"chez007", "chez008", "chez009", "chez010", "chez011", "chez012",
|
||||||
"chez013", "chez014", "chez015", "chez016",
|
"chez013", "chez014", "chez015", "chez016", "chez017",
|
||||||
"reg001"]
|
"reg001"]
|
||||||
|
|
||||||
ideModeTests : List String
|
ideModeTests : List String
|
||||||
|
19
tests/chez/chez017/Main.idr
Normal file
19
tests/chez/chez017/Main.idr
Normal file
@ -0,0 +1,19 @@
|
|||||||
|
module Main
|
||||||
|
|
||||||
|
data Foo : Type where
|
||||||
|
MkFoo : String -> Foo
|
||||||
|
|
||||||
|
data Bar : Type where
|
||||||
|
[noNewtype]
|
||||||
|
MkBar : String -> Bar
|
||||||
|
|
||||||
|
|
||||||
|
-- This code rely on the fact that `putStr` calls the Chez function `display`,
|
||||||
|
-- which allows any value to be printed. This will expose the internal
|
||||||
|
-- structure of each data type.
|
||||||
|
main : IO ()
|
||||||
|
main = do
|
||||||
|
putStr (believe_me (MkFoo "foo"))
|
||||||
|
putChar '\n'
|
||||||
|
putStr (believe_me (MkBar "bar"))
|
||||||
|
putChar '\n'
|
4
tests/chez/chez017/expected
Normal file
4
tests/chez/chez017/expected
Normal file
@ -0,0 +1,4 @@
|
|||||||
|
foo
|
||||||
|
#(0 bar)
|
||||||
|
1/1: Building Main (Main.idr)
|
||||||
|
Main> Main> Bye for now!
|
2
tests/chez/chez017/input
Normal file
2
tests/chez/chez017/input
Normal file
@ -0,0 +1,2 @@
|
|||||||
|
:exec main
|
||||||
|
:q
|
3
tests/chez/chez017/run
Executable file
3
tests/chez/chez017/run
Executable file
@ -0,0 +1,3 @@
|
|||||||
|
$1 --no-banner Main.idr < input
|
||||||
|
|
||||||
|
rm -rf build
|
Loading…
Reference in New Issue
Block a user