Thanks you very much. On 10/09/17 23:18, john.harri...@cl.cam.ac.uk wrote: > Hi Mario, > > | If you know of an existing formalization of elementary topology in HOL4 > | please let me know, so that I can avoid duplicating work. > > Not in HOL4, but in HOL Light there is quite a bit of topology, which > might at least serve as inspiration, if not something to port. See the > various files here: > > https://github.com/jrh13/hol-light/tree/master/Multivariate > > Most of it is rooted in the special case of R^n, but there is one file > with purely general topology and metric spaces: > > https://github.com/jrh13/hol-light/tree/master/Multivariate/metric.ml > > John.
-- Do not eat animals; respect them as you respect people. https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan
signature.asc
Description: OpenPGP digital signature
------------------------------------------------------------------------------ Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
