Added some lemmas about [sublist]
2 unresolved threads
2 unresolved threads
Added some generally useful lemmas about the [sublist] function
Merge request reports
Activity
Filter activity
added S-waiting-for-review label
Triage: waiting for review by @robbertkrebbers
- Resolved by Jonas Kastberg
987 987 intros; eapply elem_of_list_lookup_2. 988 988 destruct (nth_lookup_or_length l i d); [done | by lia]. 989 989 Qed. 990 Lemma elem_of_list_delete x i l : 991 x ∈ delete i l → x ∈ l. 992 Proof. - Resolved by Jonas Kastberg
- Resolved by Jonas Kastberg
Sorry for the very belated response.
I think the results in this MR make sense. I think we're still missing many of these results for the other relations (suffix, prefix, submseteq, ⊆), and ideally we make sure 1.) they are all there and consistent 2.) they are proved for the version lowest in the hierarchy and then derive the other ones. But I think even if we do not do that know, this MR provides an improvement.
added 115 commits
-
e8b54df1...e847956f - 112 commits from branch
iris:master
- 47cfb44c - Added some lemmas about [sublist]
- f5e219af - Cleaned up and renamed lemmas
- 300c1b84 - Resolved some review feedback
Toggle commit list-
e8b54df1...e847956f - 112 commits from branch
Please register or sign in to reply