fix warning: it was pointing to a record that did not exist.

agda / agda-stdlib

The Agda standard library

Other

561 stars 234 forks source link

Closed JacquesCarette closed 3 months ago

JacquesCarette commented 3 months ago

Tiny PR that fixes a silly bug.

jamesmckinna commented 3 months ago

As identified in #2299 / #2342