filtering a list cannot increase length. I tried expressing this in Idris: https://gist.github.com/johnynek/fe0a4e545f2181a6a7ed … had to cheat. Tips? /cc @edwinbrady
-
-
@edwinbrady thanks for the reply. Is the Sigma style preferred or a separate function the proves that length (filter xs fn) <= length xs? -
@posco I'm not sure to be honest. It really depends on what the result is to be used for.
End of conversation
New conversation -
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.