Stream: Coq users

Topic: ✔ Constructors with the same names


view this post on Zulip Pavel Shuhray (Apr 23 2022 at 02:35):

Hi
I want to use the same constructor's name in different inductive types

Inductive A : Set :=
| name : nat ->A.

Inductive B : Set :=
| name : nat->B.

How can I do it?

view this post on Zulip Enrico Tassi (Apr 23 2022 at 06:38):

What do you want to do in the end? Overload name?

view this post on Zulip Théo Winterhalter (Apr 23 2022 at 07:12):

The best way would be to define A and B in two different modules MA and MB and then you would be able to use MA.name and MB.name to disambiguate.

view this post on Zulip Paolo Giarrusso (Apr 23 2022 at 09:37):

Agreed; there are ways to overload functions, but AFAICT none let you overload constructors in pattern matching.

view this post on Zulip Enrico Tassi (Apr 23 2022 at 12:14):

Right, but then it is like using name1 and name2.
So why did Pavel not do it in the first place?

view this post on Zulip Paolo Giarrusso (Apr 23 2022 at 13:38):

I mean, I assume the question is about overloading name as a constructor, and the answer is "Coq has nothing that works 100%". If you give up on pattern matching, function overloading becomes relevant.

view this post on Zulip Pavel Shuhray (Apr 23 2022 at 16:59):

I have several inductive types (different types of lambda-terms) with the same constructors "var, app, lam". Lean, for example, define a new namespace for each inductive type.

view this post on Zulip Théo Winterhalter (Apr 23 2022 at 18:27):

To simulate the namespace, you can use modules then.

view this post on Zulip Théo Winterhalter (Apr 23 2022 at 18:30):

Module Foo.

  Inductive t :=
  | C (n : nat).

End Foo.

Module Bar.

  Inductive t :=
  | C (b : bool).

End Bar.

Import Foo.

Definition test_foo (x : t) :=
  match x with
  | C n => n
  end.

Definition test_bar (x : Bar.t) :=
  match x with
  | Bar.C b => b
  end.

view this post on Zulip Notification Bot (Apr 24 2022 at 14:25):

Pavel Shuhray has marked this topic as resolved.


Last updated: Jan 29 2023 at 05:03 UTC