Me gustaría poder hacer las definiciones tipo Inductive locales a la seccion, para poder reutilizar el el nombre del tipo y/o los constructores. Por lo visto, añadir 'Local', aunque compila, no funciona. Coq me sigue tirando 'list already exists' cuando la intento definir en una nueva sección.
Cual es la vuelta de tuerca?
Saludos
Hola.
En una sección podés definir variables locales, por ejemplo. Si éstas son usadas en definiciones inductivas dentro de la sección, al cerrar la sección se generalizan las definiciones donde eran usadas.
No obstante, entiendo que lo que querés hacer es otra cosa y hasta donde se, no es posible. Si definís un tipo inductivo dentro de una sección, éste queda definido más allá de la sección; no actúa como el scope tradicional de variables en los lenguajes de programación. Quizás la versión más actual de Coq tenga algo nuevo en relación a esto, pero lo dudo.
En este curso no trabajaremos con módulos de Coq (https://coq.inria.fr/distrib/current/refman/language/module-system.html).
Saludos, Carlos
