diff options
| author | Tom Smeding <tom@tomsmeding.com> | 2025-06-18 10:10:30 +0200 |
|---|---|---|
| committer | Tom Smeding <tom@tomsmeding.com> | 2025-06-18 10:10:30 +0200 |
| commit | 3db7d00b3248d746aa99f57b117d5722cbe90df0 (patch) | |
| tree | d01a0f9c1e95de07d6dc3fcb8f6895bf94a77165 /src/CHAD/Types.hs | |
| parent | 62639875102decae2bb96b3847ae48db5d1f8fd0 (diff) | |
Give DeepZero to With
Diffstat (limited to 'src/CHAD/Types.hs')
| -rw-r--r-- | src/CHAD/Types.hs | 7 |
1 files changed, 7 insertions, 0 deletions
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 |