From e7613555e2508a6dd3d9b202c030ac6a48138f5a Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 1 Dec 2021 11:53:32 -0500
Subject: [PATCH] test tele_app notation

---
 tests/telescopes.ref |  2 ++
 tests/telescopes.v   | 10 ++++++++++
 2 files changed, 12 insertions(+)

diff --git a/tests/telescopes.ref b/tests/telescopes.ref
index afac10f0..2c58e638 100644
--- a/tests/telescopes.ref
+++ b/tests/telescopes.ref
@@ -18,3 +18,5 @@
   Hγ : γ1 x
   ============================
   γ1 x ∨ γ2 x
+[TEST x y : nat, x = y]
+     : Prop
diff --git a/tests/telescopes.v b/tests/telescopes.v
index 56633586..260b7283 100644
--- a/tests/telescopes.v
+++ b/tests/telescopes.v
@@ -31,3 +31,13 @@ Proof.
 Qed.
 End tests.
 End accessor.
+
+(* Type inference for tele_app-based notation.
+(Relies on [&] bidirectionality hint of tele_app.) *)
+Definition test {TT : tele} (t : TT → Prop) : Prop :=
+  ∀.. x, t x ∧ t x.
+Notation "'[TEST'  x .. z ,  P ']'" :=
+  (test (TT:=(TeleS (fun x => .. (TeleS (fun z => TeleO)) ..)))
+        (tele_app (λ x, .. (λ z, P) ..)))
+  (x binder, z binder).
+Check [TEST (x y : nat), x = y].
-- 
GitLab