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

Improve explanation of split exercise.

Browse source
This commit is contained in:
Pedro Minicz 2019-10-26 15:45:15 -03:00
parent 1f5fe587d9
commit edd3e83581
1 changed files with 4 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1076,9 +1076,10 @@ into two lists that merge to give the original list, where all
elements of one list satisfy the predicate, and all elements of elements of one list satisfy the predicate, and all elements of
the other do not satisfy the predicate. the other do not satisfy the predicate.
Define the following variant of the traditional `filter` function on lists, Define the following variant of the traditional `filter` function on
which given a decidable predicate and a list returns all elements of the lists, which given a decidable predicate and a list returns a list of
list satisfying the predicate: 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) (zs : List A) split : ∀ {A : Set} {P : A → Set} (P? : Decidable P) (zs : List A)
→ ∃[ xs ] ∃[ ys ] ( merge xs ys zs × All P xs × All (¬_ ∘ P) ys ) → ∃[ xs ] ∃[ ys ] ( merge xs ys zs × All P xs × All (¬_ ∘ P) ys )