diff options
| author | Chloe Brown <chloe.brown.00@outlook.com> | 2023-04-15 17:07:32 +0100 |
|---|---|---|
| committer | Chloe Brown <chloe.brown.00@outlook.com> | 2023-04-15 17:07:32 +0100 |
| commit | 9e2bd48420feba7c7752fd98cdf10fb67f56edc8 (patch) | |
| tree | def22eb937657d68ee54e3ed7222ebb62fc1d9c5 /src/Core/Term | |
| parent | 5313058dcdd7252dbaa5615df2494368fe7c32f9 (diff) | |
Define declarative typing rules.
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 |