El usuario podrá pre-ejecutar el código siguiendo el chequeo sintáctico realizado (Req. 2.3.5) y avanzar de un error a otro paso a paso (esta funcionalidad es ofrecida por el F7 en el CoqIDE). De la misma manera, puede intentar compilar el código (Req. 2.1.11) y visualizar los errores encontrados durante la compilación.
Anonymous