4.69mi. 1:05:00 HR 138 (avg.)
Search
4 results for “boydstephensmithjr”
-
I think I made measurable progress today on my sized-sequences library
I wish I had test coverage tools for #idris, but my property tests make it fairly clear that cons and unsnoc and snoc work.
Still have some long (but not interesting) proofs to write for append. Also thinking of making `reverse` constant time, but I'm not sure it can be a simple flag the way it is for reversable, appendable deques in the literature.
-
Anyone have an #NetBSD VPS provider? I've done a few searches myself, but each time I get to the configuration stage, there's no NetBSD option.
I don't need it for much, but I would like to get my personal email and web hosting off of LInux. It has to be a VPS (or something equivalent) with IPv4 access, because neither static IPs nor IPv6 access are available from my Internet provider, and unless I want to throw in with Starlink, they are the only provider in the area.
I am not confident I could install NetBSD remotely, as I've only installed NetBSD once, and even then I messed up the networking during that process. I am fairly sure I can migrate my existing dovecot+exim+spamassassin and apache setups once I have ssh+su root access to a system with working network configuration.
-
I think I'm actually getting better at proving things in #idris but it's still overly painful.
There's too many situations where the unifier gives up with an error about a hole where there's a good way to fill the hole to make unification succeed.
Often it's trivial. Unification would succeed if the named hole was replaced with an unnamed hole. So, I think the unifier should emit some sort of diagnostic, but then proceed with the as if / under the assumption that the named hole replaced with the value that would be used for an unnamed hole.
Other times it is still easy, a suitable value in scope could fill the hole but something else (? no axiom K ?) is preventing that value from even being proposed by expression search when asked. Manually replacing the hole with the bound name causes unification to succeed, (? After using the binding allows further reductions in normal form?)
OT: Do any of my no-AI followers know how to get idris2-lsp working with vim-classic ?