Forked from
Iris / Iris
Source project has a limited visibility.
-
Robbert Krebbers authored
and `frac_auth_frag_valid_op_1_l`, add `frac_auth_frag_op_validN` and `frac_auth_frag_op_valid`, which are bi-implications with arbitrary fractions.
Robbert Krebbers authoredand `frac_auth_frag_valid_op_1_l`, add `frac_auth_frag_op_validN` and `frac_auth_frag_op_valid`, which are bi-implications with arbitrary fractions.
