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!
I'm very thankful for the the judgement forms in the boxes though - it does ease some of the burden, and I find it harder when papers omit them. I just found it a bit of a struggle to remember how to parse stuff when going back and forth between pages.
Makes me wonder if more uniform notations are helpful when systems approach a certain level of complexity - also some sort of interactivity might have helped too, perhaps?
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!
1
2
Show replies
You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more
You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more