- 15 May, 2018 3 commits
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
- 14 May, 2018 1 commit
-
-
Robbert Krebbers authored
-
- 11 May, 2018 1 commit
-
-
Ralf Jung authored
fix `head_stuck` See merge request FP/iris-coq!144
-
- 09 May, 2018 8 commits
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
-
- 08 May, 2018 2 commits
- 07 May, 2018 3 commits
-
-
Robbert Krebbers authored
- Make `flöb_pre` and `flöb` local to the proof. - The metavariables `Ψ` are used for predicates, so use a `Q` here.
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
- 04 May, 2018 1 commit
-
-
Ralf Jung authored
-
- 03 May, 2018 8 commits
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
It now turns the goal into `P` and `<pers> Q`, which is dual to `iDestruct`, which turns `P ∧ <pers> Q` into `P` and `□ Q`.
-
Robbert Krebbers authored
-
Ralf Jung authored
This follows the proof at https://en.wikipedia.org/wiki/L%C3%B6b's_theorem#Proof_of_L%C3%B6b's_theorem
-
Ralf Jung authored
-
Robbert Krebbers authored
-
Glen Mével authored
-
- 27 Apr, 2018 4 commits
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Ralf Jung authored
-
Ralf Jung authored
-
- 25 Apr, 2018 5 commits
- 24 Apr, 2018 3 commits
- 23 Apr, 2018 1 commit
-
-
Ralf Jung authored
-