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?
What do you want to do in the end? Overload name
?
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.
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: Oct 13 2024 at 01:02 UTC