From 2f06a480fe180d7a2ef8b575da157a06ccf817a9 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 31 Oct 2015 18:32:11 -0700
Subject: [PATCH] test(tests/lean/run/partial_explicit): add test for '@@'
 operator

---
 tests/lean/run/partial_explicit.lean | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)
 create mode 100644 tests/lean/run/partial_explicit.lean

diff --git a/tests/lean/run/partial_explicit.lean b/tests/lean/run/partial_explicit.lean
new file mode 100644
index 0000000000..cf5b3d2d33
--- /dev/null
+++ b/tests/lean/run/partial_explicit.lean
@@ -0,0 +1,18 @@
+section
+variables a b c : nat
+variable  H1 : a = b
+variable  H2 : a + b + a + b = 0
+
+example : b + b + a + b = 0 :=
+  @@eq.rec_on (λ x, x + b + a + b = 0) H1 H2
+end
+
+section
+variables (f : Π {T : Type₁} {a : T} {P : T → Prop}, P a → Π {b : T} {Q : T → Prop}, Q b → Prop)
+variables (T : Type₁) (a : T) (P : T → Prop) (pa : P a)
+variables (b : T) (Q : T → Prop) (qb : Q b)
+
+check @f T a P pa b Q qb -- Prop
+check @@f P pa Q qb      -- Prop
+check f pa qb            -- Prop
+end