Skip to content
  • Ralf Jung's avatar
    Change the sharing view shift to frame a token · acddfae5
    Ralf Jung authored
    This also needs changes in type and continuation context inclusion.
    It allows us to prove that the empty sum is equal to the empty type.
    I also took the opportunity to rename TCtx_holds to TCtx_hasty, which at least says what is "holding".
    acddfae5