search

UlfNorell / agda-test

Agda test
0 stars 0 forks source link

add to Library All (¬_ ∘ P) xs iff ¬ Any P xs (?) #904

Closed UlfNorell closed 10 years ago

UlfNorell commented 10 years ago

From mech...@botik.ru on September 18, 2013 15:53:00

This is a question on Standard library. Has it sense to add this relation between All and Any:

All (¬_ ∘ P) xs iff ¬ Any P xs ?

Original issue: http://code.google.com/p/agda/issues/detail?id=904

UlfNorell commented 10 years ago

From nils.anders.danielsson on September 19, 2013 06:34:58

I've included this result in Data.List.All.Properties.

Status: Fixed

UlfNorell commented 10 years ago

From nils.anders.danielsson on September 19, 2013 06:38:48

Labels: Library

UlfNorell commented 10 years ago

From andres.s...@gmail.com on November 11, 2013 06:24:01

Labels: Type-Enhancement