Home - News ( United States | United Kingdom | Italy | Germany ) - Football scores

Showing content from https://github.com/agda/agda/issues/2004 below:

`DISPLAY` should be more pragmatic · Issue #2004 · agda/agda · GitHub

I’d like to use Data.List.Any from the standard library and have readable goals. I tried the following, but was rebuked:

{-# DISPLAY Any (_≡_ x) Y = x ∈ Y #-}

Could not parse the left-hand side Any (_≡_ x) Y
Operators used in the grammar:
None
when scope checking the left-hand side Any (_≡_ x) Y in the
definition of Any

The only documentation for DISPLAY says lambdas are not allowed. I’m not sure if (_≡_ x) qualifies as a lambda; it seems like a partially-applied defined function to me.

RetroSearch is an open source project built by @garambo | Open a GitHub Issue

Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo

HTML: 3.2 | Encoding: UTF-8 | Version: 0.7.4