Add ability to desugar terms.

Remove `getChildren` construct---it's too niche for the core language.

1 files changed, 7 insertions, 0 deletions

diff --git a/src/Inky/Data/SnocList/Quantifiers.idr b/src/Inky/Data/SnocList/Quantifiers.idr
index 73c6551..ac6287b 100644
--- a/src/Inky/Data/SnocList/Quantifiers.idr
+++ b/src/Inky/Data/SnocList/Quantifiers.idr
@@ -4,6 +4,8 @@ import public Data.SnocList.Quantifiers
 
 import Data.List.Quantifiers
 import Inky.Data.Irrelevant
+import Inky.Data.SnocList
+import Inky.Data.SnocList.Elem
 import Inky.Decidable
 
 public export
@@ -41,6 +43,11 @@ relevant [<] _ = [<]
 relevant (sx :< x) prfs = relevant sx (tail prfs) :< Forget (head prfs)
 
 public export
+tabulate : LengthOf sx -> (forall x. Elem x sx -> p x) -> All p sx
+tabulate Z f = [<]
+tabulate (S len) f = tabulate len (f . There) :< f Here
+
+public export
 data Pairwise : (a -> a -> Type) -> SnocList a -> Type where
   Lin : Pairwise r [<]
   (:<) : Pairwise r sx -> All (flip r x) sx -> Pairwise r (sx :< x)