fromInteger for universe

2022-05-08 20:02:21 +02:00 · 2022-05-08 20:02:21 +02:00 · 756bc5b9f3
parent 41056559f2
commit 756bc5b9f3
1 changed files with 4 additions and 0 deletions
--- 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