program_logic/lifting.v · 7b619dd36b8b3b2d4bc7f8e0f2db02880ee3f3df · Ike Mulder / Iris

Forked from Iris / Iris

Source project has a limited visibility.

8 years ago

Lifting lemmas do no longer have in hypothsesis that the expression is not a value. · 7b619dd3

Jacques-Henri Jourdan authored 8 years ago

This fact is deduced from reducibility. Unfortunately, this sometimes depends on the type of states being inhabited, so that this additional hypothesis sometimes appear.

7b619dd3

History

Lifting lemmas do no longer have in hypothsesis that the expression is not a value.

Jacques-Henri Jourdan authored 8 years ago

This fact is deduced from reducibility. Unfortunately, this sometimes depends on the type of states being inhabited, so that this additional hypothesis sometimes appear.