Hola, quería saber si podemos usar el operador pipe, tal como se ve en el siguiente esquema del tutorial de Coq:
T; [T1 | T2 | ... | Tn]
Gracias!
Saludos!
Si, claro.
La semántica es la siguiente:
Se ejecutan las tácticas T1...Tn a cada uno de los subgoals (en orden) que surgen al ejecutar la táctica T.
Una variante más simple del punto y como (;) es: T1;T2. Aquí se ejecuta la táctica T2 al goal que surge de aplicar primero la táctica T1.
Saludos, Carlos