agda / cubical

An experimental library for Cubical Agda
https://agda.github.io/cubical/Cubical.README.html
Other
446 stars 136 forks source link

Remove redundant third constructor to replacement #1087

Closed ecavallo closed 7 months ago

ecavallo commented 7 months ago

The last constructor in the current inductive-recursive definition of replacement is unnecessary. Thanks go to @dwarn and @plt-amy who independently pointed this out to me some time ago.

mortberg commented 7 months ago

Nice!