variadic binders for Pi, SIgma and lambda

CoqHott · Dec 14, 2023 · 787fe43 · 787fe43
1 parent 6fa27fd
commit 787fe43
Show file tree

Hide file tree

Showing 2 changed files with 14 additions and 5 deletions.
diff --git a/theories/Decidability/Execution.v b/theories/Decidability/Execution.v
@@ -68,15 +68,15 @@ 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.
 
 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.
diff --git 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).