summaryrefslogtreecommitdiff
path: root/src/CHAD/Types.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/CHAD/Types.hs')
-rw-r--r--src/CHAD/Types.hs7
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