michael/csci8980-f21
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

merge

Browse source
This commit is contained in:
wadler 2019-11-12 21:05:11 +00:00
commit 38cd3659ca
1 changed files with 6 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/plfa/part1/Lists.lagda.md
View file

@ -1089,12 +1089,13 @@ into two lists that merge to give the original list, where all
elements of one list satisfy the predicate, and all elements of
the other do not satisfy the predicate.
Define the following variant of the traditional `filter` function on lists,
which given a decidable predicate and a list returns all elements of the
list satisfying the predicate:
Define the following variant of the traditional `filter` function on
lists, which given a decidable predicate and a list returns a list of
elements that satisfy the predicate and a list of elements that don't,
with their corresponding proofs.
split : ∀ {A : Set} {P : A → Set} (P? : Decidable P) (xs : List A)
→ ∃[ ys ] ∃[ zs ] ( merge xs ys zs × All P ys × All (¬_ ∘ P) zs )
split : ∀ {A : Set} {P : A → Set} (P? : Decidable P) (zs : List A)
→ ∃[ xs ] ∃[ ys ] ( merge xs ys zs × All P xs × All (¬_ ∘ P) ys )
```
-- Your code goes here