Skip to content
GitLab

Step-indexed propositions

Merged Robbert Krebbers requested to merge robbert/sprop into master

Following the discussions on Iris-club, hereby a merge request for siProp. I created this file already a long time ago, but never did do anything with it.

This MR:

  • Defines the type siProp of step-indexed propositions
  • Defines the operators of an intuitionistic logic + equality + later.
  • Proves the basic laws of these operators.
  • Proves soundness statements.
  • Shows that siProp forms an SBI so we get support in the proofmode.
Edited by Robbert Krebbers