Add simple test for implicit binding around quotes

madman-bob · Aug 7, 2020 · e73fdac · e73fdac
1 parent 8f54466
commit e73fdac
Showing 1 changed file with 6 additions and 0 deletions.
diff --git a/tests/idris2/reflection004/refdecl.idr b/tests/idris2/reflection004/refdecl.idr
@@ -4,6 +4,12 @@ import Language.Reflection
 
 %language ElabReflection
 
+fc : FC
+fc = EmptyFC
+
+quoteTest : TTImp -> TTImp -> List Decl
+quoteTest f arg = `[ myFunc : ~(IApp fc f arg) ]
+
 axes : (n : Nat) -> {auto gt : GT n 0} -> {auto lte : LTE n 4} -> Vect n String
 axes 1 = ["x"]
 axes 2 = "y" :: axes 1