New answers tagged

0 votes

Is there a way to rename parameters when including/reusing a module type in Coq?

Notation are not part of the module type. So you need to make it a definition. But if you put a definition in a module type then you must comply to it exactly in the module. So the definition of ...
Pierre Courtieu's user avatar

Top 50 recent answers are included