search

plfa / plfa.github.io

An introduction to programming language theory in Agda
https://plfa.github.io
Creative Commons Attribution 4.0 International
1.37k stars 315 forks source link

`_⊎_` from Connectives.agda no longer compiles in 2.6.4 #1023

Closed JacquesCarette closed 2 months ago

JacquesCarette commented 2 months ago

The problem is that the definition confuses parameters and indicies. The "correct" definition would be

data _⊎_ (A : Set) (B : Set) : Set where

  inj₁ : 
      A
      -----
    → A ⊎ B

  inj₂ :
      B
      -----
    → A ⊎ B

(which is what is essentially in the standard library)

wadler commented 2 months ago

I'm confused. What is in the book currently is:

data _⊎_ (A B : Set) : Set where

  inj₁ :
      A
      -----
    → A ⊎ B

  inj₂ :
      B
      -----
    → A ⊎ B

(a) That compiles fine under 2.6.4.1. (b) I don't see how it differs from your suggested correction.

JacquesCarette commented 2 months ago

My error! I apparently had some older versions of the files around which did have that "bug". I see that this is indeed fixed now.

Looks like I'm going to have to rebuild all my live-coding, full-of-holes Agda files from scratch from current PLFA. Glad that I caught it now instead of during a lecture...

wadler commented 2 months ago

OK. Thanks for checking.