A RetroSearch Logo

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

Search Query:

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

DISPLAY form on irrelevant projection drops arguments · Issue #7825 · agda/agda · GitHub

While reviewing PR #7824:

{-# OPTIONS --irrelevant-projections #-}
{-# OPTIONS --show-irrelevant #-}

record Wrap (A : Set) : Set where
  field theWrapped : A

record Squash (A : Set) : Set where
  field .theSquashed : A

postulate
  RELEVANT   : Set
  IRRELEVANT : Set

{-# DISPLAY Wrap.theWrapped    _ = RELEVANT   #-}
{-# DISPLAY Squash.theSquashed _ = IRRELEVANT #-}

postulate
  P : {A : Set} → .A → Set

_ : P Wrap.theWrapped
_ = {!!}

_ : P Squash.theSquashed
_ = {!!}

-- ?0 : P (λ r → RELEVANT)  -- correct
-- ?1 : P IRRELEVANT        -- wrong, should be P (λ r → IRRELEVANT)

pappToTerm uses hand-knitted code to calculated the number of parameters and this is no longer correct for irrelevant projections since PR #5815 (Agda 2.6.2.2):

pars = case theDef def of Constructor { conPars = p } -> p Function { funProjection = Right Projection{projIndex = i} } | i > 0 -> i - 1 _ -> 0

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