@@ -88,18 +88,25 @@ wfInd {rel} step x = accInd step x (wellFounded {rel} x)
8888-- Some basic useful relations
8989
9090||| LT is a well-founded relation on numbers
91−ltAccessible : (m : Nat) -> LT n m -> Accessible LT n
92−ltAccessible Z x = absurd x
93−ltAccessible (S k) (LTESucc x)
94− = Access (\val, p => ltAccessible k (lteTransitive p x))
91+ltAccessible : (n : Nat) -> Accessible LT n
92+ltAccessible n = Access (\v, prf => ltAccessible' {n'=v} n prf)
93+ where
94+ ltAccessible' : (m : Nat) -> LT n' m -> Accessible LT n'
95+ ltAccessible' Z x = absurd x
96+ ltAccessible' (S k) (LTESucc x)
97+ = Access (\val, p => ltAccessible' k (lteTransitive p x))
9598
9699-- First list is smaller than the second
97100smaller : List a -> List a -> Type
98101smaller xs ys = LT (length xs) (length ys)
99102
100103||| `smaller` is a well-founded relation on lists
101−smallerAcc : (ys : List a) -> smaller xs ys -> Accessible smaller xs
102−smallerAcc [] x = absurd x
103−smallerAcc (y :: ys) (LTESucc x)
104− = Access (\val, p => smallerAcc ys (lteTransitive p x))
104+smallerAcc : (xs : List a) -> Accessible WellFounded.smaller xs
105+smallerAcc xs = Access (\v, prf => smallerAcc' {xs'=v} xs prf)
106+ where
107+ smallerAcc' : (ys : List a) -> smaller xs' ys -> Accessible smaller xs'
108+ smallerAcc' [] x = absurd x
109+ smallerAcc' (y :: ys) (LTESucc x)
110+ = Access (\val, p => smallerAcc' ys (lteTransitive p x))
111+
105112