@@ -101,25 +101,11 @@ SizeAccessible = Accessible Smaller
101101||| Proof of well-foundedness of `Smaller`.
102102||| Constructs accessibility for any given element of `a`, provided `Sized a`.
103103sizeAccessible : Sized a => (x : a) -> SizeAccessible x
104−sizeAccessible x = Access $ f (size x) (ltAccessible $ size x)
104+sizeAccessible x = Access (acc $ size x)
105105 where
106− -- prove well-foundedness of `Smaller` from well-foundedness of `LT`
107− f : (sizeX : Nat) -> (acc : Accessible LT sizeX)
108− -> (y : a) -> (size y `LT` sizeX) -> SizeAccessible y
109− f Z acc y pf = absurd pf
110− f (S n) (Access acc) y (LTESucc yLEx)
111− = Access (\z, zLTy =>
112− f n (acc n $ LTESucc lteRefl) z (lteTransitive zLTy yLEx)
113− )
114−
115− ||| LT is a well-founded relation on numbers
116− ltAccessible : (n : Nat) -> Accessible LT n
117− ltAccessible n = Access (\v, prf => ltAccessible' {n'=v} n prf)
118− where
119− ltAccessible' : (m : Nat) -> LT n' m -> Accessible LT n'
120− ltAccessible' Z x = absurd x
121− ltAccessible' (S k) (LTESucc x)
122− = Access (\val, p => ltAccessible' k (lteTransitive p x))
106+ acc : (sizeX : Nat) -> (y : a) -> (size y `LT` sizeX) -> SizeAccessible y
107+ acc (S x') y (LTESucc yLEx')
108+ = Access (\z, zLTy => acc x' z (lteTransitive zLTy yLEx'))
123109
124110||| Strong induction principle for sized types.
125111sizeInd : Sized a