0 | ||| WellFounded on List suffixes
 1 | module Data.List.Sufficient
 2 |
 3 | import Control.WellFounded
 4 |
 5 | %default total
 6 |
 7 | public export
 8 | data Suffix : (ys,xs : List a) -> Type where
 9 |   IsSuffix : (x : a) -> (zs : List a)
10 |           -> (0 ford : xs = x :: zs ++ ys) -> Suffix ys xs
11 |
12 | SuffixAccessible : (xs : List a) -> Accessible Suffix xs
13 | SuffixAccessible [] = Access (\y => \case (IsSuffix x zs _) impossible)
14 | SuffixAccessible ws@(x :: xs) =
15 |   let fact1@(Access f) = SuffixAccessible xs
16 |   in Access $ \ys => \case
17 |     (IsSuffix x [] Refl) => fact1
18 |     (IsSuffix x (z :: zs) Refl) => f ys (IsSuffix z zs Refl)
19 |
20 | public export
21 | WellFounded (List a) Suffix where
22 |   wellFounded = SuffixAccessible
23 |