diff --git a/GenerateEverything.hs b/GenerateEverything.hs index 73945759df..13d06bc3ed 100644 --- a/GenerateEverything.hs +++ b/GenerateEverything.hs @@ -134,8 +134,10 @@ sizedTypesModules = map modToFile , "Data.Container.Any" , "Data.Container.FreeMonad" , "Data.Nat.PseudoRandom.LCG.Unsafe" + , "Data.Tree.Binary.Show" , "Data.Tree.Rose" , "Data.Tree.Rose.Properties" + , "Data.Tree.Rose.Show" , "Data.Trie" , "Data.Trie.NonEmpty" , "Relation.Unary.Sized" diff --git a/src/Data/Tree/Binary/Show.agda b/src/Data/Tree/Binary/Show.agda index 9fd3f7ccf9..9544ac06b4 100644 --- a/src/Data/Tree/Binary/Show.agda +++ b/src/Data/Tree/Binary/Show.agda @@ -4,7 +4,7 @@ -- 1 dimensional pretty printing of binary trees ------------------------------------------------------------------------ -{-# OPTIONS --without-K --safe --sized-types #-} +{-# OPTIONS --without-K --sized-types #-} open import Level using (Level) open import Data.List.Base as List using (List; []; [_]; _∷_; _∷ʳ_) diff --git a/src/Data/Tree/Rose/Show.agda b/src/Data/Tree/Rose/Show.agda index 69fdee845d..74727b6830 100644 --- a/src/Data/Tree/Rose/Show.agda +++ b/src/Data/Tree/Rose/Show.agda @@ -4,7 +4,7 @@ -- 1 dimensional pretty printing of rose trees ------------------------------------------------------------------------ -{-# OPTIONS --without-K --safe --sized-types #-} +{-# OPTIONS --without-K --sized-types #-} module Data.Tree.Rose.Show where