Commit 6d2ac942 authored by Ralf Jung's avatar Ralf Jung
Browse files

Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coq

parents 18cce8d0 fff4fc98
......@@ -49,7 +49,7 @@ algebra/agree.v
algebra/excl.v
algebra/iprod.v
algebra/functor.v
program_logic/upred.v
algebra/upred.v
program_logic/model.v
program_logic/adequacy.v
program_logic/hoare_lifting.v
......
(** This file is essentially a bunch of testcases. *)
Require Import program_logic.upred program_logic.ownership.
Require Import program_logic.ownership.
Require Import heap_lang.lifting heap_lang.sugar.
Import heap_lang uPred notations.
......
......@@ -331,12 +331,11 @@ Proof.
rewrite ?coPset_elem_of_node; naive_solver.
* by intros [q' ->]; induction q; simpl; rewrite ?coPset_elem_of_node.
Qed.
Lemma coPset_suffixes_infinite p : ¬set_finite (coPset_suffixes p).
Proof.
rewrite coPset_finite_spec; simpl.
(* FIXME no time to finish right now, but I think it holds *)
Abort.
induction p; simpl; rewrite ?coPset_finite_node, ?andb_True; naive_solver.
Qed.
(** * Splitting of infinite sets *)
Fixpoint coPset_l_raw (t : coPset_raw) : coPset_raw :=
......
Require Export program_logic.upred program_logic.resources.
Require Export algebra.upred program_logic.resources.
Require Import algebra.cofe_solver.
(* The Iris program logic is parametrized by a functor from the category of
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment