[Agda] map⊆

Nils Anders Danielsson nad at cse.gu.se
Fri Oct 10 18:04:17 CEST 2014


On 2014-10-10 17:44, Sergei Meshveliani wrote:
> And I wonder of whether all this is inventing a bicycle.
> Can  map⊆  be expressed in a simpler way?
> What Standard library has for all this?

See Data.List.Any.Membership.map-mono, which is restricted to
propositional equality.

-- 
/NAD



More information about the Agda mailing list