Skip to content
Snippets Groups Projects

Add `submsetseq` function

Open Add `submsetseq` function
marijnvanwezel/stdpp:marijnvanwezel/permutations_submseteq into master
1 unresolved thread
Open Marijn van Wezel requested to merge marijnvanwezel/stdpp:marijnvanwezel/permutations_submseteq into master
1 unresolved thread

This merge requests adds the submsetseq function, which for a list l computes all lists l' such that l' ⊆+ l. It also adds a new lemma about interleave.

Edited by Marijn van Wezel

Merge request reports

Loading
Loading

Activity

Filter activity
  • Approvals
  • Assignees & reviewers
  • Comments (from bots)
  • Comments (from users)
  • Commits & branches
  • Edits
  • Labels
  • Lock status
  • Mentions
  • Merge request status
  • Tracking
stdpp/list.v
337 337 Infix "⊆+" := submseteq (at level 70) : stdpp_scope.
338 338 Global Hint Extern 0 (_ ⊆+ _) => reflexivity : core.
339 339
340 (** The function [submsetseq l] yields all lists [l'] such that [l' ⊆+ l]. *)
341 Fixpoint submsetseq {A} (l : list A) : list (list A) :=
  • Ralf Jung
  • Marijn van Wezel added 1 commit

    added 1 commit

    • cd9c6a5c - Prove iff lemma for elem_of_interleave

    Compare with previous version

  • Marijn van Wezel changed the description

    changed the description

  • Marijn van Wezel mentioned in merge request !594 (merged)

    mentioned in merge request !594 (merged)

  • Marijn van Wezel added 13 commits

    added 13 commits

    Compare with previous version

  • Marijn van Wezel added 1 commit

    added 1 commit

    • f16275c6 - Add `submsetseq` and associated lemmas

    Compare with previous version

    • Please register or sign in to reply