mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2024-09-11 16:05:51 +03:00
Add test for Double subtraction
This commit is contained in:
parent
479872290d
commit
a70c68da91
@ -40,6 +40,7 @@ idrisTests
|
||||
"interface005", "interface006", "interface007", "interface008",
|
||||
"interface009", "interface010", "interface011", "interface012",
|
||||
"interface013", "interface014",
|
||||
"interpreter001",
|
||||
"lazy001",
|
||||
"linear001", "linear002", "linear003", "linear004", "linear005",
|
||||
"linear006", "linear007",
|
||||
|
2
tests/idris2/interpreter001/expected
Normal file
2
tests/idris2/interpreter001/expected
Normal file
@ -0,0 +1,2 @@
|
||||
Main> 1.5
|
||||
Main> Bye for now!
|
2
tests/idris2/interpreter001/input
Normal file
2
tests/idris2/interpreter001/input
Normal file
@ -0,0 +1,2 @@
|
||||
3.5 - 2.0
|
||||
:q
|
1
tests/idris2/interpreter001/run
Executable file
1
tests/idris2/interpreter001/run
Executable file
@ -0,0 +1 @@
|
||||
$1 --no-banner < input
|
Loading…
Reference in New Issue
Block a user