From 2aa29d4bf5c6cac8fc0a470fd12dfd1cc8e0cffd Mon Sep 17 00:00:00 2001 From: Kiana Sheibani Date: Mon, 6 Mar 2023 10:59:05 -0500 Subject: [PATCH] Fix visibility in Data.Tensor --- Data/Tensor.idr | 1 + 1 file changed, 1 insertion(+) diff --git a/Data/Tensor.idr b/Data/Tensor.idr index 35d25c5..df8b03f 100644 --- a/Data/Tensor.idr +++ b/Data/Tensor.idr @@ -57,6 +57,7 @@ export Symmetric Either where swap = either Right Left +export Tensor Either Void where unitl = MkIso (either absurd id) Right unitr = MkIso (either id absurd) Left