Hello! I'm trying to define a notation with a binder that only should be bound in part of the right-hand side and I don't know how to do it. Here's a simple example where it fails:

```
From Coq Require Import Utf8.
Section Foo.
Context (M : ∀ (A : Type) (B : A → Type), Type).
Notation "∇ x , B" :=
(∀ x, M _ B)
(at level 200, x binder).
Fail Check ∇ x, x = 0.
```

If I apply `B`

to `x`

explicitly in the notation it also complains.

you mean

```
Notation "∇ x , B" :=
(M _ (fun x => B))
(at level 200, x binder).
```

?

I guess the problem is I want something weird. You made me realise, `x`

in my notation is bound twice and what I want is:

```
Notation "∇ x , B" :=
(∀ x, M _ (λ x, B))
(at level 200, x binder).
```

and it seems to work. Thanks.

For some reason though, `∇ (x : nat), x = 0`

is printed as `∇ x0, x0 = 0`

…

Also for `∇ x, x = 0`

it doesn't infer the type of `x`

is there any way to say the binders should have the same types?

how's the first `x`

possibly used before being shadowed? This prints without renaming:

```
Notation "∇ x , B" :=
(∀ _, M _ (λ x, B))
(at level 200, x binder).
Check ∇ x, x = 0.
```

regarding shared types, it seems you can ask via named evars and `refine`

, but type inference doesn't seem too happy.

This _might_ relate to the previous problem, but I thought the idea was maybe still worth sharing...

```
From Coq Require Import Utf8.
Section Foo.
Context (M : ∀ (A : Type) (B : A → Type), Type).
Notation "∇ x , B" :=
(∀ x, M _ (λ x, B))
(only printing, at level 200, x binder).
Let x : Type.
refine (∀ x : ?[T], M _ (λ x : ?T, x = 0)).
Defined.
Fail Notation "∇ x , B" :=
(∀ x : ?T, M ?[T] (λ x, B))
(only parsing, at level 200, x binder).
Notation "∇ x , B" :=
(* ltac:(refine (∀ x : ?[T], M _ (λ x : ?T, B))) *)
ltac:(refine (∀ x : ?[T], M _ (λ x : ?T, x = 0)))
(only parsing, at level 200, x binder).
Fail Check (∇ x, x = 0).
(*
Error: In environment
M : ∀ A : Type, (A → Type) → Type
x := ∇ x0, x0 = 0 : Type
The term "0" has type "nat" while it is expected to have type "Type".
*)
```

EDIT: clarified snippet

Yeah, I guess what I wanted didn't make much sense, and that's reasonable that it's not properly supported.

Last updated: Jun 15 2024 at 05:01 UTC