[Practico 5] Ejercicio 7 - notación ";".

[Practico 5] Ejercicio 7 - notación ";".

de Bruno Rolando Boz -
Número de respuestas: 1

Buenas,

Necesito cambiar el scope de ";", definido en ej6, para poder usarlo en ej7.
Estoy usando Infix ";" := ... :export. Esto me tira un warning: 

Declaring a scope implicitly is deprecated; use in advance an explicit
"Declare Scope export.". [undeclared-scope,deprecated]

No me doy cuenta como cambiar el scope correctamente.

Agradecería la ayuda.

Saludos.

En respuesta a Bruno Rolando Boz

Re: [Practico 5] Ejercicio 7 - notación ";".

de Carlos Luna -

Hola.

No tengo claro si cambió algo en la última versión de Coq pero en cada sección que lo uses entiendo que podés poner algo como:

Infix "simbolo" := cons_instr (at level 60, right associativity). (* donde cons_instr es el constructor correspondiente en LInstr *)

Saludos, Carlos