Estimados estudiantes,
Les recordamos que está publicado el material para la última entrega del curso.
Para trabajar con mappings, pueden basarse en la biblioteca Maps.v que se incluye junto con la letra del práctico, o directamente usar las funciones de Coq. Para definir una función parcial de un tipo A a un tipo B, puede usarse el tipo option:
Inductive option (T : Type) : Type :=
Some : T -> option T | None : option T
Esto es, f : A -> option B.
Saludos, Carlos