diff options
Diffstat (limited to 'src/Core/Term')
| -rw-r--r-- | src/Core/Term/Thinned.idr | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/Core/Term/Thinned.idr b/src/Core/Term/Thinned.idr index 824439a..3ed4779 100644 --- a/src/Core/Term/Thinned.idr +++ b/src/Core/Term/Thinned.idr @@ -22,6 +22,11 @@ record Thinned (n : Nat) where %inline public export +pure : Term n -> Thinned n +pure = (`Over` id n) + +%inline +public export expand : Thinned n -> Term n expand (term `Over` thin) = wkn term thin |