summaryrefslogtreecommitdiff
path: root/src/Encoded/Union.idr
diff options
context:
space:
mode:
authorChloe Brown <chloe.brown.00@outlook.com>2023-06-21 16:05:44 +0100
committerChloe Brown <chloe.brown.00@outlook.com>2023-06-21 16:05:44 +0100
commit0ddaf1b2c9ca66cf0ae03d2f6ad792c7885dfc32 (patch)
tree8dac25792a00c24aa1d55288bb538fab89cc0092 /src/Encoded/Union.idr
parentaf7c222cc3e487cd3ca8b5dd8749b7e258da7c7c (diff)
Add sums, vectors and arithmetic encodings.
Also define pretty printing of terms.
Diffstat (limited to 'src/Encoded/Union.idr')
-rw-r--r--src/Encoded/Union.idr2
1 files changed, 2 insertions, 0 deletions
diff --git a/src/Encoded/Union.idr b/src/Encoded/Union.idr
index 5c3b95c..00b07e7 100644
--- a/src/Encoded/Union.idr
+++ b/src/Encoded/Union.idr
@@ -2,6 +2,8 @@ module Encoded.Union
import Term.Syntax
+-- Binary Union ----------------------------------------------------------------
+
export
(<+>) : Ty -> Ty -> Ty
N <+> N = N