idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-11-24 06:52:19 +03:00
Code Issues Projects Releases Wiki Activity

Forgot to add the new test again, didn't I...

Browse Source
This commit is contained in:
Edwin Brady 2020-06-01 19:13:46 +01:00
parent 3d2765e930
commit 1c18fe589b
4 changed files with 27 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
tests/idris2/reflection005/expected Normal file
View File

@ -0,0 +1,9 @@
1/1: Building refdecl (refdecl.idr)
refdecl.idr:13:16--14:1:While processing right hand side of bad at refdecl.idr:13:1--14:1:
When unifying Elab () and Elab TT
Mismatch between:
()
and
TT
Main> 9400
Main> Bye for now!

2
tests/idris2/reflection005/input Normal file
View File

@ -0,0 +1,2 @@
mkMult 100
:q

13
tests/idris2/reflection005/refdecl.idr Normal file
View File

@ -0,0 +1,13 @@
import Language.Reflection
%language ElabReflection
mkDecls : TTImp -> Elab ()
mkDecls v
= declare `[ mkMult : Int -> Int
mkMult x = x * ~(v) ]
%runElab mkDecls `(94)
bad : a
bad = %runElab mkDecls `(94)

3
tests/idris2/reflection005/run Executable file
View File

@ -0,0 +1,3 @@
$1 --no-banner refdecl.idr < input
rm -rf build