- Jun 11, 2019
-
-
Ralf Jung authored
-
Ralf Jung authored
change frac_auth notation See merge request iris/iris!259
-
Ralf Jung authored
-
Robbert Krebbers authored
-
Jacques-Henri Jourdan authored
The unbounded fractional authoritative camera See merge request iris/iris!187
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
The unbounded fractional authoritative camera is a version of the fractional authoritative camera that can be used with fractions `> 1`. Most of the reasoning principles for this version of the fractional authoritative cameras are the same as for the original version. There are two difference: - We get the additional rule that can be used to allocate a "surplus", i.e. if we have the authoritative element we can always increase its fraction and allocate a new fragment. ✓ (a ⋅ b) → ●U{p} a ~~> ●U{p + q} (a ⋅ b) ⋅ ◯U{q} b - At the cost of that, we no longer have the `◯U{1} a` is an exclusive fragmental element (cf. `frac_auth_frag_validN_op_1_l`).
-
Robbert Krebbers authored
-
- Jun 10, 2019
-
-
Ralf Jung authored
-
Ralf Jung authored
-
Robbert Krebbers authored
Add ghost data to locations See merge request iris/iris!249
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
- Jun 09, 2019
-
-
Ralf Jung authored
Fix regression with iSpecialize errors. See merge request iris/iris!262
-
Joseph Tassarotti authored
-
Ralf Jung authored
Fix error messages for iSplitL/iSplitR. See merge request iris/iris!261
-
Joseph Tassarotti authored
-
Ralf Jung authored
-
Ralf Jung authored
-
- Jun 07, 2019
-
-
Robbert Krebbers authored
-
Ralf Jung authored
-
- Jun 06, 2019
- Jun 05, 2019
-
-
Robbert Krebbers authored
Alternative take on making proof mode terms more compact. See merge request iris/iris!254
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-