From 079c7aa62d66ac5be21f01b352ec0243bb53b7f9 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Wed, 14 Feb 2024 14:38:00 +0000 Subject: [PATCH] fixed `sized-types` error in orphan module --- doc/README/Data/Tree/Binary.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/README/Data/Tree/Binary.agda b/doc/README/Data/Tree/Binary.agda index cf7e2de90a..0f03ad7b79 100644 --- a/doc/README/Data/Tree/Binary.agda +++ b/doc/README/Data/Tree/Binary.agda @@ -4,7 +4,7 @@ -- Some examples showing how the Binary tree module can be used ------------------------------------------------------------------------ -{-# OPTIONS --cubical-compatible --safe --sized-types #-} +{-# OPTIONS --cubical-compatible --sized-types #-} module README.Data.Tree.Binary where