Thanks, Vince! I think you're saying that the HOL4 Q-module can do type inference using the goal. I would guess that Petros's IsabelleLight techniques (which I used for my consider) could also do this goal-powered type inference. Freek's miz3.ml does much more type inference.
Specifically, if OCaml has some curried expression F X Y Z, then it will evaluate Z, then Y, then X before it evaluates the overall expression. Thanks, Mark! I didn't know that, and I'd wondered about it. But this is only barely relevant. However, this involves designing a proof scripting language and writing a parser for it That's kind of what Freek' miz3.ml does, and Vince has been instructing me on how to do similar things. I didn't that like Isabelle's Isar was similar... -- Best, Bill ------------------------------------------------------------------------------ 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 hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
