## Stream: Coq users

### Topic: Notation with binder only in part of the right-hand side

#### Théo Winterhalter (Feb 24 2023 at 08:24):

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.

#### Laurent Théry (Feb 24 2023 at 09:02):

you mean

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

?

#### Théo Winterhalter (Feb 24 2023 at 09:21):

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.

#### Théo Winterhalter (Feb 24 2023 at 09:27):

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?

#### Paolo Giarrusso (Feb 24 2023 at 12:17):

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.
``````

#### Paolo Giarrusso (Feb 24 2023 at 12:25):

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

#### Théo Winterhalter (Feb 24 2023 at 12:28):

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