From ecaf9deb4b1d2ce85617438e621690b2df3ea367 Mon Sep 17 00:00:00 2001 From: Greg Brown Date: Tue, 12 Nov 2024 16:44:31 +0000 Subject: Add ability to desugar terms. Remove `getChildren` construct---it's too niche for the core language. --- src/Inky/Data/SnocList/Quantifiers.idr | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'src/Inky/Data/SnocList/Quantifiers.idr') 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 @@ -40,6 +42,11 @@ relevant : (sx : SnocList a) -> (0 prfs : All p sx) -> All (Irrelevant . p) sx 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 [<] -- cgit v1.2.3