From 787fe43cf20e63469f16d30cf4ab33d400d8ccdd Mon Sep 17 00:00:00 2001
From: Kenji Maillard <kenji@maillard.blue>
Date: Mon, 18 Sep 2023 09:27:45 +0200
Subject: [PATCH] variadic binders for Pi, SIgma and lambda

---
 theories/Decidability/Execution.v |  4 ++--
 theories/TermNotations.v          | 15 ++++++++++++---
 2 files changed, 14 insertions(+), 5 deletions(-)

diff --git a/theories/Decidability/Execution.v b/theories/Decidability/Execution.v
index f6f99bfa..022c843a 100644
--- a/theories/Decidability/Execution.v
+++ b/theories/Decidability/Execution.v
@@ -68,7 +68,7 @@ Qed.
 
 Check ((fun x => nat_rec (fun _ => nat) 0 (fun _ ih => S (S ih)) x) : nat -> nat).
 
-Goal ⟪ε |- λ ℕ, indℕ ℕ 0 (λ ℕ, λ ℕ, x₀.+2) 2 : ℕ → ℕ⟫.
+Goal ⟪ε |- λ ℕ, indℕ ℕ 0 (λ ℕ ℕ, x₀.+2) 2 : ℕ → ℕ⟫.
 Proof.
   infer_auto.
 Qed.
@@ -76,7 +76,7 @@ Qed.
 Check (eq_refl : (nat_rect (fun _ => Type) nat (fun _ ih => nat -> ih) 3) = (nat -> nat -> nat -> nat)).
 
 Goal ⟪ ε |- rfl □ (ℕ → ℕ → ℕ → ℕ) :
-  (ℕ → ℕ → ℕ → ℕ) =⟨ □ ⟩ indℕ □ ℕ (λ ℕ, λ □, ℕ → x₀) 3⟫.
+  (ℕ → ℕ → ℕ → ℕ) =⟨ □ ⟩ indℕ □ ℕ (λ ℕ □, ℕ → x₀) 3⟫.
 Proof.
   check_auto.
 Qed.
\ No newline at end of file
diff --git a/theories/TermNotations.v b/theories/TermNotations.v
index 5a3b632d..4d751a66 100644
--- a/theories/TermNotations.v
+++ b/theories/TermNotations.v
@@ -32,10 +32,16 @@ Notation "'x₉'" := (tRel 9) (in custom mltt at level 0).
 Notation "'□'" := U (in custom mltt at level 0).
 
 (* Π fragment *)
-Notation "'Π' A , B" := (tProd A B) (in custom mltt at level 2, right associativity).
+(* Notation "'Π' A , B" := (tProd A B) (in custom mltt at level 2, right associativity). *)
+Notation "'Π' x .. y , p" := (tProd x ( .. (tProd y p) ..))
+  (in custom mltt at level 2, x, y at level 0, right associativity,
+   format "'[' 'Π'  '/  ' x  ..  y ,  '/  ' p ']'").
 Notation "A '→' B" := (tProd A B⟨↑⟩) (in custom mltt at level 2, right associativity).
 Notation "f x" := (tApp f x) (in custom mltt at level 1, left associativity).
-Notation "'λ' A , t" := (tLambda A t) (in custom mltt at level 2, right associativity).
+(* Notation "'λ' A , t" := (tLambda A t) (in custom mltt at level 2, right associativity). *)
+Notation "'λ' x .. y , p" := (tLambda x ( .. (tLambda y p) ..))
+  (in custom mltt at level 2,  x, y at level 0, right associativity,
+   format "'[' 'λ'  '/  ' x  ..  y ,  '/  ' p ']'").
 
 (* Nat fragment *)
 Notation "'ℕ'" := tNat (in custom mltt at level 0).
@@ -54,7 +60,10 @@ Notation "4" := ⟪tm 0.+4⟫ (in custom mltt at level 0).
 Notation "5" := ⟪tm 0.+5⟫ (in custom mltt at level 0).
 
 (* Σ fragment *)
-Notation "'∑' A , B" := (tSig A B) (in custom mltt at level 2, right associativity).
+Notation "'∑' x .. y , p" := (tSig x ( .. (tSig y p) ..))
+  (in custom mltt at level 2,  x, y at level 0, right associativity,
+   format "'[' '∑'  '/  ' x  ..  y ,  '/  ' p ']'").
+(* Notation "'∑' A , B" := (tSig A B) (in custom mltt at level 2, right associativity). *)
 Notation "A '×' B" := (tSig A B⟨↑⟩) (in custom mltt at level 2).
 Notation "( x : A ; y : B )" := (tPair A B x y) (in custom mltt at level 0, x, A, y, B at level 2).
 Notation "x '.1'" := (tFst x) (in custom mltt at level 1).