[ test ] added test for eta expansion of singleton record instance ar…

…guments
agda · Oct 28, 2015 · 4bac556 · 4bac556
1 parent 9abefe5
commit 4bac556
Showing 1 changed file with 11 additions and 0 deletions.
diff --git a/test/succeed/SingletonInstance.agda b/test/succeed/SingletonInstance.agda
@@ -0,0 +1,11 @@
+
+module _ where
+
+record ⊤ : Set where
+  constructor tt
+
+f : {{u : ⊤}} → ⊤
+f = _
+
+foo : (x : ⊤) → ⊤
+foo x = f