Idris2-boot icon indicating copy to clipboard operation
Idris2-boot copied to clipboard

"Undefined name filter"

Open Pytheas01 opened this issue 5 years ago • 1 comments

If possible, please include complete self contained source files (for example by uploading to https://gist.github.com) that exhibit the issue in addition to quoting from them here. The smaller the example the better!

Steps to Reproduce

filter (\ARG => ARG < 3) [0, 1, 2, 3, 4]

Expected Behavior

[0, 1, 2] : List Integer

Observed Behavior

(interactive):1:1--1:41:Undefined name filter

Pytheas01 avatar Apr 04 '20 06:04 Pytheas01

That's right, filter isn't in the prelude, it's in Data.List.

edwinb avatar Apr 06 '20 14:04 edwinb