­jonoodle­ @ionchy@types.pl

@132ikl they both look the same

WAIT I think I'm talking about ANF translation
Or monadic form, since I don't care if my lets are nested

@jordyd yeah... if I did it the solve-later way it'd be a metavariable (for sizes, which is what I'm thinking about specifically rn), but I think it might be possible to just bind the solutions in the theory itself to let expressions? But I'd have to do it backwards though, like go through function application arguments in reverse order

I think I just described a let expression

It's more like, if you compile a term from left to right, sometimes I'll introduce a variable and I won't know what to substitute it with just yet, but I promise that by the time I've compiled the whole thing I'll know what should go in there

Can I add a constraint solver to a compiler? Just a little one, as a treat
It's not really constraints when the only constraint is equality and uniqueness

Of ANF fame
I thought they were a woman this whole time?? I just didn't check??

Wait is Amr Sabry not a woman?

​
I forgot we had this

does the f*ck emoji go under Miscellaneous

@hazel j'accuse

okay who added ​

​

@vdash https://twitter.com/jonmsterling/status/1382453125114630144
he's saying things again

Agda's record syntax and copatterns make a surprising amount of intuitive sense once you've used them a bit
I think I need to unlearn Coq's old coinductives because it's poisoning how I'm supposed to think about them

Amount of physics taken: 5 years
Amount of physics remembered: 0 years

@david eddy currents
idk who eddy is