mirror of
https://github.com/ilyakooo0/Idris-dev.git
synced 2024-11-15 01:25:05 +03:00
New test
This commit is contained in:
parent
397542cd3e
commit
2342656792
6
test/test005/expected
Normal file
6
test/test005/expected
Normal file
@ -0,0 +1,6 @@
|
||||
8
|
||||
sO
|
||||
(abc, 123)
|
||||
(abc, 123)
|
||||
([1, 2], [3, 4, 5])
|
||||
([1, 2], [3, 4, 5])
|
4
test/test005/run
Executable file
4
test/test005/run
Executable file
@ -0,0 +1,4 @@
|
||||
#!/bin/bash
|
||||
idris test005.idr -o test005
|
||||
./test005
|
||||
rm -f test005 test005.ibc
|
16
test/test005/test005.idr
Normal file
16
test/test005/test005.idr
Normal file
@ -0,0 +1,16 @@
|
||||
module main;
|
||||
|
||||
tstr : String;
|
||||
tstr = "abc123";
|
||||
|
||||
tlist : List Int;
|
||||
tlist = [1, 2, 3, 4, 5];
|
||||
|
||||
main : IO ();
|
||||
main = do { print (abs (-8));
|
||||
print (abs (S O));
|
||||
print (span isAlpha tstr);
|
||||
print (break isDigit tstr);
|
||||
print (span (\x => x < 3) tlist);
|
||||
print (break (\x => x > 2) tlist);
|
||||
};
|
Loading…
Reference in New Issue
Block a user