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