add Dim.toConst

2022-04-06 20:32:56 +02:00 · 2022-04-06 20:32:56 +02:00 · e6d942ce1b
parent 2c1ca7e19b
commit e6d942ce1b
1 changed files with 5 additions and 0 deletions
--- a/src/Quox/Syntax/Dim.idr
+++ b/src/Quox/Syntax/Dim.idr
@ -50,6 +50,11 @@ PrettyHL (Dim n) where
  prettyM (B i) = prettyVar DVar DVarErr (!ask).dnames i


+public export %inline
+toConst : Dim 0 -> DimConst
+toConst (K e) = e
+
+
 public export
 DSubst : Nat -> Nat -> Type
 DSubst = Subst Dim