From 41d1c4a059466833325320e1d494d99af9d36cb2 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Thu, 22 Jun 2023 13:52:03 +0100
Subject: WIP: define semantics in Idris.

---
 src/Term/Semantics.idr | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'src/Term/Semantics.idr')

diff --git a/src/Term/Semantics.idr b/src/Term/Semantics.idr
index 2e61040..dd76f62 100644
--- a/src/Term/Semantics.idr
+++ b/src/Term/Semantics.idr
@@ -10,6 +10,7 @@ TypeOf : Ty -> Type
 TypeOf N = Nat
 TypeOf (ty ~> ty') = TypeOf ty -> TypeOf ty'
 
+public export
 rec : Nat -> a -> (a -> a) -> a
 rec 0 x f = x
 rec (S k) x f = f (rec k x f)
@@ -66,3 +67,8 @@ fullSem' (Rec (MakePair t (MakePair u v _ `Over` thin) _)) = do
 export
 sem : Term ty ctx -> All TypeOf ctx -> TypeOf ty
 sem t = runIdentity (sem' t)
+
+export
+arb : (ty : Ty) -> TypeOf ty
+arb N = 0
+arb (ty ~> ty') = const (arb ty')
-- 
cgit v1.2.3