From 0ddaf1b2c9ca66cf0ae03d2f6ad792c7885dfc32 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Wed, 21 Jun 2023 16:05:44 +0100
Subject: Add sums, vectors and arithmetic encodings.

Also define pretty printing of terms.
---
 src/Encoded/Fin.idr | 48 ++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 48 insertions(+)
 create mode 100644 src/Encoded/Fin.idr

(limited to 'src/Encoded/Fin.idr')

diff --git a/src/Encoded/Fin.idr b/src/Encoded/Fin.idr
new file mode 100644
index 0000000..901c612
--- /dev/null
+++ b/src/Encoded/Fin.idr
@@ -0,0 +1,48 @@
+module Encoded.Fin
+
+import public Data.Nat
+
+import Data.Stream
+import Encoded.Arith
+import Encoded.Pair
+import Term.Semantics
+import Term.Syntax
+
+export
+Fin : Nat -> Ty
+Fin k = N
+
+oldShow : Nat -> String
+oldShow = show
+
+export
+zero : Term (Fin (S k)) ctx
+zero = Zero
+
+export
+suc : Term (Fin k ~> Fin (S k)) ctx
+suc = Abs' Suc
+
+export
+inject : Term (Fin k ~> Fin (S k)) ctx
+inject = Id
+
+export
+absurd : {ty : Ty} -> Term (Fin 0 ~> ty) ctx
+absurd = Arb
+
+export
+induct : {ty : Ty} -> Term (Fin (S k) ~> ty ~> (Fin k * ty ~> ty) ~> ty) ctx
+induct = rec
+
+export
+forget : Term (Fin k ~> N) ctx
+forget = Id
+
+export
+allSem : (k : Nat) -> List (TypeOf (Fin k))
+allSem k = take k nats
+
+export
+divmod' : (k : Nat) -> {auto 0 ok : NonZero k} -> Term (N ~> N * Fin k) ctx
+divmod' k = Abs' (\n => App divmod [<n, Lit k])
-- 
cgit v1.2.3