[FRIAM] talk about rabbit holes ...

[Jon Zingale]

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.

Jon
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://redfish.com/pipermail/friam_redfish.com/attachments/20200327/4e0b3dcf/attachment.html>