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?
What do you want to do in the end? Overload
The best way would be to define
B in two different modules
MB and then you would be able to use
MB.name to disambiguate.
Agreed; there are ways to overload functions, but AFAICT none let you overload constructors in pattern matching.
Right, but then it is like using name1 and name2.
So why did Pavel not do it in the first place?
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.
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.
To simulate the namespace, you can use modules then.
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.
Pavel Shuhray has marked this topic as resolved.
Last updated: Jan 29 2023 at 05:03 UTC