Commit 72833963 by Michael Sammler

### fix build

parent b2a8a82c
Pipeline #51180 passed with stage
in 24 minutes and 32 seconds
 ... ... @@ -10,7 +10,7 @@ Qed. Lemma same_length_lookup_Some {A B} (l1 : list A) (l2 : list B) (i : nat) (v : A): length l1 = length l2 → l1 !! i = Some v → is_Some (l2 !! i). Proof. move => Hlen H. eapply same_length_lookup => //. by exists v. move => Hlen H. by eapply same_length_lookup. Qed. Lemma StronglySorted_app {A} {R : A → A → Prop} `{!Transitive R} l1 l2 : ... ... @@ -316,7 +316,7 @@ Section defs. btree_invariant o r n ks vs cs → ∀ k, k ∈ ks → br_min r ≤ k ≤ br_max r. Proof. move => Hinv k Hk. apply elem_of_list_lookup in Hk as [i Hk]. assert (br_map r ≠ ∅). { eapply btree_invariant_has_key_non_empty => //. exists k. exact Hk. } { by eapply btree_invariant_has_key_non_empty. } rewrite /btree_invariant bool_decide_true // /= in Hinv. destruct Hinv as (Hlen&->&_&_&_&_&_&HSS&HB&_&_&_&_&_&Heq). apply HB. assert (is_Some (vs !! i)) as [v Hv] by by eapply same_length_lookup_Some. ... ...
 ... ... @@ -834,7 +834,7 @@ Section typing. iIntros "Hs Hv". iDestruct (i2p_proof with "Hs Hv") as (Q) "[HQ HT]" => /=. simpl in *. iApply ("HT" with "HQ"). Qed. Global Instance typed_if_simplify_inst ot v (P T1 T2 : iProp Σ) n {SH : SimplifyHyp P (Some n)}: Global Instance typed_if_simplify_inst ot v (P : iProp Σ) n {SH : SimplifyHyp P (Some n)}: TypedIf ot v P | 1000 := λ T1 T2, i2p (typed_if_simplify ot v P T1 T2 n). ... ...
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!