[Iris-Club] Two Monoid Questions
Robbert Krebbers
mailinglists at robbertkrebbers.nl
Fri Aug 16 14:27:32 CEST 2019
On 8/16/19 2:24 PM, Ralf Jung wrote:
> I would define SProp, but not need a proof-mode instance or so.
By defining SProp, I suppose you would also define the logical operators
and prove that it's an step-indexed intuitionistic logic? Once you have
all of that, it's actually trivial to show that it's a proof-mode
instance (I think I can do that in an hour or so).
More information about the Iris-Club
mailing list