I can't imagine he'd try to extend his "helper functions" that far, no. I wasn't even familiar with Prover9 until I saw that post: https://www.cs.unm.edu/~mccune/mace4/ It's a small world after all.
On 3/27/20 10:35 AM, Marcus Daniels wrote: > There’s the singletons library for GHC, and some follow-on work for Dependent > Haskell. As far as I can tell it is another one of those drawn-out projects > that the Haskell community manages to endure/ignore. > > On 3/27/20 9:45 AM, Jon Zingale wrote: >> Glen, >> >> It is kind of funny to me, and yet should not surprise me, that an >> individual was motivated to write a theorem prover in R. OTOH, >> every attempt I have ever made to get Agda to work for me has >> required sandboxing my Haskell environments and switching to >> an emacs editor, so hey. Still, the project strikes me as being one >> of bull headedness, a just-to-see-if-one-can kind of thing. >> >> Do you think they will go so far as to implement general dependent >> typing? Last night at some point, I was thinking about the problem of >> implementing flexible contravariant functors in a computing language. >> This often appears to a stumbling block when I set out to define /for all/ >> and /there exists/ from a substitution functor, a la Topos theory. >> Any thoughts are welcome. -- ☣ uǝlƃ ============================================================ FRIAM Applied Complexity Group listserv Meets Fridays 9a-11:30 at cafe at St. John's College to unsubscribe http://redfish.com/mailman/listinfo/friam_redfish.com archives back to 2003: http://friam.471366.n2.nabble.com/ FRIAM-COMIC http://friam-comic.blogspot.com/ by Dr. Strangelove
