@@ -101,12 +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)
104+sizeAccessible x = Access (acc $ size x)
105105 where
106− -- prove well-foundedness of `Smaller` from well-foundedness of `LT`
107− f : (sizeX : Nat) -> (y : a) -> (size y `LT` sizeX) -> SizeAccessible y
108− f (S x') y (LTESucc yLEx')
109− = Access (\z, zLTy => f x' z (lteTransitive zLTy yLEx'))
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'))
110109
111110||| Strong induction principle for sized types.
112111sizeInd : Sized a