PL twitter: quick, what's the scariest screenshot you can find of a paper with an overwhelming amount of inference rules?
22
25
82
Conversation
I am so thankful for the existence of this paper so I feel rather bad posting it, but I did find that all the different notations at play kind of overloaded my brain!
4
3
6
This particular page also overloaded my own brain at several times while writing it :P
1
4
Specifying something as complicated as dependent pattern elaboration using natural deduction definitely is no small feat! But as somebody trying to implement this stuff I'm thankful you wrote it, as it puts lots of stuff together in one place!
Trying to figure out how elaboration works involves a lots of cobbling together bits and pieces from different places, and trying to dig into implementations, so it's super nice to have higher level descriptions of this stuff!
4