Dear HOL users,
Is there any support in HOL for defining coinductive relations?
If not, is there at least an example where it was done "manually"?
If not, would anyone be interested in sketching out what would be required,
and possibly working on it with me? Probably at least some of the Hol_reln
machinery could be reused.
Cheers,
Ramana
------------------------------------------------------------------------------
Precog is a next-generation analytics platform capable of advanced
analytics on semi-structured data. The platform includes APIs for building
apps and a phenomenal toolset for data science. Developers can use
our toolset for easy data analysis & visualization. Get a free account!
http://www2.precog.com/precogplatform/slashdotnewsletter
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
