program_logic · d1ef32dda9f4a410db34d8244bfb5489cac9f09a · Ike Mulder / Iris · GitLab

Snippets Groups Projects

Forked from Iris / Iris

6025 commits behind the upstream repository.

Uniform syntax for selecting hypotheses.

Robbert Krebbers authored 8 years ago

Used in iRevert, iClear, iFrame, and for generalizing the IH in
iInduction and iLöb.

d1ef32dd

d1ef32dd 8 years ago

Name	Last commit	Last update
..
adequacy.v
auth.v
boxes.v
cancelable_invariants.v
counter_examples.v
ectx_language.v
ectx_lifting.v
ectxi_language.v
ghost_ownership.v
hoare.v
invariants.v
iris.v
language.v
lifting.v
model.v
namespaces.v
ownership.v
pviewshifts.v
saved_prop.v
sts.v
thread_local.v
viewshifts.v
weakestpre.v