From 756bc5b9f38bcd6ccfc0fb49b0ed11d282545ee9 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Sun, 8 May 2022 20:02:21 +0200
Subject: [PATCH] fromInteger for universe

---
 lib/Quox/Syntax/Universe.idr | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/lib/Quox/Syntax/Universe.idr b/lib/Quox/Syntax/Universe.idr
index 10d6075..7a84161 100644
--- a/lib/Quox/Syntax/Universe.idr
+++ b/lib/Quox/Syntax/Universe.idr
@@ -21,3 +21,7 @@ export
 PrettyHL Universe where
   prettyM UAny  = pure $ hl Delim "_"
   prettyM (U l) = pure $ hl Free $ pretty l
+
+export %inline
+fromInteger : (x : Integer) -> (0 _ : So (x >= 0)) => Universe
+fromInteger x = U $ fromInteger x