Skip to content
  • Robbert Krebbers's avatar
    Large refactoring. · deb6d9e5
    Robbert Krebbers authored
    - Protocols are no longer contractive in the message
    - New type `iMsg` for messages to avoid telescopes in protocols
    - Better rules for subprotocols that do not involve telescopes, but allow introduction
      and elimination of quantifiers and the payload
    - Better notations for protocols
    - Notation ⊑ for subprotocols
    - Make ⊑ except-0 so one can strip laters when proving a ⊑
    - Restore recursive domain equation to push later inwards to support protocols
      that are not contractive in the mssage.
    - Proofmode support for easy manipulation of ⊑
    deb6d9e5