From f64047b9ac748e2031dc7afe0a3d27aa3491589c Mon Sep 17 00:00:00 2001 From: Denis Buzdalov Date: Tue, 17 Oct 2023 14:45:52 +0300 Subject: [PATCH] [ safe ] Set deriving escape hatches to be marked as `%unsafe` --- libs/base/Deriving/Common.idr | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/libs/base/Deriving/Common.idr b/libs/base/Deriving/Common.idr index c002b62832..b305fcf8f0 100644 --- a/libs/base/Deriving/Common.idr +++ b/libs/base/Deriving/Common.idr @@ -18,7 +18,7 @@ data IsFreeOf : (x : Name) -> (ty : TTImp) -> Type where TrustMeFO : IsFreeOf a x ||| We may need to manufacture proofs and so we provide the `assert` escape hatch. -export +export -- %unsafe -- uncomment as soon as 0.7.0 is released assert_IsFreeOf : IsFreeOf x ty assert_IsFreeOf = TrustMeFO @@ -165,7 +165,7 @@ data HasImplementation : (intf : a -> Type) -> TTImp -> Type where TrustMeHI : HasImplementation intf t ||| We may need to manufacture proofs and so we provide the `assert` escape hatch. -export +export -- %unsafe -- uncomment as soon as 0.7.0 is released assert_hasImplementation : HasImplementation intf t assert_hasImplementation = TrustMeHI