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

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

`--postfix-projections` do not make use of mixfix syntax · Issue #7318 · agda/agda · GitHub

Consider the testcase for #2288:

record Setoid : Set₁ where
  field
    ∣_∣    : Set
    {{eq}} : Eq ∣_∣
open Setoid

NatSetoid : Setoid
∣ NatSetoid ∣ = Nat

The error with --no-postfix-projections is:

No instance of type Eq ∣ NatSetoid ∣ ...

With --postfix-projections we get:

No instance of type Eq (NatSetoid .∣_∣)

This isn't pretty. Postfix notation should not kick in when we can actually use the mixfix-syntax.

A little doubt: the field ∣_∣ : Set is actually a hack, exploiting the questionable "feature" of Agda to blindly apply mixfix syntax even when outside the module it was defined in.

• Printing of infix/mixfix operators defined in parametrized modules #632

So maybe the current broken postfix printing is less wrong than the prefix printing.

Opinions?

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