mangoiv

@jaror perhaps it would help to not have it be collocated with ICFP which seems to be quite inaccessible.

@jaror tell me 😳

@jaror yeah it seems fine at first; issue is that someone probably has to do the theory part, writing a new papers for every one new addition seems tedious 😅

@jaror will this interact with any future proposals towards DH? I’m worried that this increase the pile of chores one would have to do to finally reach the goal of implementing them, similarly to how it happened with LinearTypes (and multiplicity polymorphism ftm) themselves.

@jaror https://media.discordapp.net/attachments/905224379120615424/1154597600788500550/F6lZ9TDbMAAxFX2.png perhaps interesting to know. The first guy is who did foundation. Very responsible lmao

@jaror https://lean-fro.org/

@jaror my bet is on him joining the lean4 fro

@jaror second one was even more awesome than the first one! This view is something that makes it really possible to argue for laziness by default! Thank you @lexi_lambda!

@jaror oh yeah much better. Lovely, thanks ;)

@jaror I’d deem it more elegant if there were any useful names in here eh

@jaror it also exhibited a bug in the byte code interpreter which had been found before

@jaror yes very nasty, I reported an issue and three bugs were found investigating it. Romes and Ben did great work doing so. It were multiple issues with pointer tagging.