From 3db7d00b3248d746aa99f57b117d5722cbe90df0 Mon Sep 17 00:00:00 2001 From: Tom Smeding Date: Wed, 18 Jun 2025 10:10:30 +0200 Subject: Give DeepZero to With --- src/CHAD/Types.hs | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'src/CHAD/Types.hs') diff --git a/src/CHAD/Types.hs b/src/CHAD/Types.hs index 8b3a8db..e061588 100644 --- a/src/CHAD/Types.hs +++ b/src/CHAD/Types.hs @@ -126,6 +126,13 @@ lemZeroInfoScal STF32 = Refl lemZeroInfoScal STF64 = Refl lemZeroInfoScal STBool = Refl +lemDeepZeroInfoScal :: SScalTy t -> DeepZeroInfo (D2s t) :~: TNil +lemDeepZeroInfoScal STI32 = Refl +lemDeepZeroInfoScal STI64 = Refl +lemDeepZeroInfoScal STF32 = Refl +lemDeepZeroInfoScal STF64 = Refl +lemDeepZeroInfoScal STBool = Refl + d1Identity :: STy t -> D1 t :~: t d1Identity = \case STNil -> Refl -- cgit v1.2.3-70-g09d2