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

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

Error TooManyPolarities is too eager · Issue #7851 · agda/agda · GitHub

• Pricing

Assignees

open import Agda.Builtin.Equality

interleaved mutual

  Sort : Set₁
  Sort = _

  postulate
    A : Sort

  {-# POLARITY A ++ #-}

  _ : Sort ≡ (Set → Set)
  _ = refl

error: [TooManyPolarities]
Too many polarities given in the POLARITY pragma for A (at most 0 allowed).

I suggest to turn this error into a warning which can then be ignored in the present case.

You can’t perform that action at this time.

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