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

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

Irrelevance in the type of a record module definition · Issue #6270 · agda/agda · GitHub

Consider the following code:

record R : Set where
  A : Set₁
  A = Set

The type of R.A uses irrelevance:

Modules
Names
  A : .R → Set₁

Why is this the case? If you add a trivial field to R, then the type of R.A no longer uses irrelevance:

open import Agda.Builtin.Unit

record R : Set where
  field
    x : ⊤

  A : Set₁
  A = Set

Modules
Names
  A : R → Set₁
  x : R → ⊤

Ordinary modules are not treated in this way:

module _ where

module M (_ : Set) where
  A : Set₁
  A = Set

Modules
Names
  A : Set → Set₁

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