You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
constructability only says that we have enough type rules. it doesn't say that we've made good on our "not outside in claim". i wonder if there's a metatheorem that would act as a checksum on that. (and therefore would catch stuff like the case rules we missed in sums and @cyrus- found last last week)
The text was updated successfully, but these errors were encountered:
maybe it's "if you can do an action in the synthetic position at the top level, you should be able to do it anywhere". not true for the current calculus, but aspirational. I think you need funny judgements about "does not analyze" and "does not have matched arrow type" and so on to really get this to work.
constructability only says that we have enough type rules. it doesn't say that we've made good on our "not outside in claim". i wonder if there's a metatheorem that would act as a checksum on that. (and therefore would catch stuff like the
case
rules we missed in sums and @cyrus- found last last week)The text was updated successfully, but these errors were encountered: