[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