­jonoodle­ @ionchy@types.pl

$\mathcal{things ~ are ~ just ~ other ~ things}$

(rest (rest (rest input)))... that is cdddr

a b c d
a b c
  b c d
1 2 3 4

yeah... first and fourth

Or.. first and third? I can't count

If I take the sum of three elements and then subtract the sum of the three elements one element before it, isn't that just the difference between the first and fourth elements

What if I dragged people in the lab into AoC

Love this animals [for/list] https://github.com/ionathanch/adventofcode-2021/blob/main/src/01.rkt

Unfortunately I have done it

someone STOP ME

no no no I can't do AoC this year. I have applications to finish and a paper to edit

Tomorrow's task: make this pretty and hopefully take also makes it clear
Tonight's task: ...well I've already played Minecraft so idk

I regret to announce that in an attempt to clarify, I have instead obfuscated

Am I suppose to understand the algorithms I use? Haven't understood it for two years I don't think I'll start understanding now

*I'm a grandmotha voice* I'm an engiNEER

I've looked at a few others' statements and for some reason they're full of Things They've Done
Like the first page will just be entirely describing the work they've done
I mean I did the same, but my master's statement was definitely not half full of what I've done

Time for MINECRAFT ​

Okay took me long enough to add just a little bit of technical material and to finalize the non-technical stuff
I'll print them out, let them sit, and then submit tmrw

Furthermore it might be the case that one cannot compile full cubical type theory without some kind of performance overhead, due to the fact that some computation rules involve computation under binders.

Isn't normalization of the body of a lambda computation under a binder? I guess running a program just never does that? ??

We restrict certain cubical features: Glue and higher constructors may only be used in code
that will be erased by the compiler.

I guess this is the same as saying no computational behaviour relies on the cubical bits

How exactly do you get a dependently typed language compiler that is correct wrt to programs running to equivalent outputs but with erased types