Remove the bad constructor on coinductive types

agda · Jan 24, 2024 · 86b5233 · 86b5233
1 parent 573426b
commit 86b5233
Showing 1 changed file with 1 addition and 2 deletions.
diff --git a/Cubical/Codata/Conat/Base.agda b/Cubical/Codata/Conat/Base.agda
@@ -1,4 +1,4 @@
-{- Conatural numbers (Tesla Ice Zhang, Feb. 2019)
+{- Conatural numbers (Tesla Zhang, Feb. 2019)
 
 This file defines:
 
@@ -30,7 +30,6 @@ record Conat : Type₀
 Conat′ = Unit ⊎ Conat
 record Conat where
   coinductive
-  constructor conat′
   field force : Conat′
 open Conat public