Skip to content

Make authoritative part of auth fractional

Hai Dang requested to merge haidang/iris:frac_auth into master

This follows #42 (closed). Somewhat related is #114 (closed).

This replaces Auth's carrier from Ex(M) to Frac * Ag(M). There are now 3 types of elements: ●{q} a, ◯ b, and ● a ≡ ●{1} a.

Cons: due to using Ag, Auth is not complete anymore, and does not enjoy Leibniz equality.

I tried to maintain the same interface of auth, and so far only lemmas concerning valid change interfaces. Changes to keep Iris built is very small (build tested locally with master at 8.9).

What do you think? @jung @robbertkrebbers @jjourdan @janno

Edited by Ralf Jung

Merge request reports