@@ -101,23 +101,12 @@ 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 (f $ size x)
105105 where
106106 -- 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 (S n) (Access acc) y (LTESucc yLEx)
110− = Access (\z, zLTy =>
111− f n (acc n $ LTESucc lteRefl) z (lteTransitive zLTy yLEx)
112− )
113−
114− ||| LT is a well-founded relation on numbers
115− ltAccessible : (n : Nat) -> Accessible LT n
116− ltAccessible n = Access (\v, prf => ltAccessible' {n'=v} n prf)
117− where
118− ltAccessible' : (m : Nat) -> LT n' m -> Accessible LT n'
119− ltAccessible' (S k) (LTESucc x)
120− = Access (\val, p => ltAccessible' k (lteTransitive p x))
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'))
121110
122111||| Strong induction principle for sized types.
123112sizeInd : Sized a