Skip to content

Un ejemplo de uso de Coq y Agda para lemas triviales sobre árboles binarios.

License

Notifications You must be signed in to change notification settings

mroman42/recorridosArboles

Repository files navigation

Recorridos en Árboles

Un ejemplo de uso de Coq para probar lemas triviales sobre árboles binarios.
Los teoremas se exponen, se explican y se demuestran en el archivo recorrido_reflejado.pdf, generado desde recorrido_reflejado.tex. La implementación en Coq de las definiciones y demostraciones se hace en treeTraversal.v.

About

Un ejemplo de uso de Coq y Agda para lemas triviales sobre árboles binarios.

Topics

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published