Hola,
La duda surge del ejercicio 17 del práctico 4. El ejercicio maneja la notación ++ para el append y << para la relación de posfijo. Mi duda es cómo definir las notaciones infijas cuando las variables de tipo en la función "append" o en la relación "posfijo" (definidas previamente) son explícitas.
Por ejemplo, si la variable de tipo es implícita
Inductive posfijo {A:Set} : list A -> list A -> Prop := ...
entonces puedo definir la notación << como
Notation "l1 << l2" := (posfijo l1 l2) (at level 50).
o como
Infix "<<" := (posfijo)(left associativity, at level 94).
(De hecho, por lo que leí en el manual, Infix es equivalente a Notation: https://coq.inria.fr/refman/user-extensions/syntax-extensions.html#the-infix-command)
Sin embargo, si la variable de tipo es explícita
Inductive posfijo (A:Set) : list A -> list A -> Prop := ...