@@ -86,14 +86,19 @@ wfInd : WellFounded rel => {P : a -> Type} ->
86wfInd {rel} step x = accInd step x (wellFounded {rel} x)
86wfInd {rel} step x = accInd step x (wellFounded {rel} x)
89−-- Accessibility for sized types
89+||| Interface of types with sized values.
91+||| The sizes are used for proofs of termination via accessibility.
93+||| @ a the type whose elements can be mapped to Nat
91interface Sized a where
94interface Sized a where
92 size : a -> Nat
95 size : a -> Nat
94Smaller : Sized a => a -> a -> Type
97Smaller : Sized a => a -> a -> Type
95Smaller x y = size x `LT` size y
98Smaller x y = size x `LT` size y
100+||| Proof of well-foundedness of `Smaller`.
101+||| Constructs accessibility for any given element of `a`, provided `Sized a`.
97accessible : Sized a => (x : a) -> Accessible Smaller x
102accessible : Sized a => (x : a) -> Accessible Smaller x
98accessible x = Access $ f (size x) (ltAccessible $ size x)
103accessible x = Access $ f (size x) (ltAccessible $ size x)
@@ -114,6 +119,7 @@ accessible x = Access $ f (size x) (ltAccessible $ size x)
114 ltAccessible' (S k) (LTESucc x)
119 ltAccessible' (S k) (LTESucc x)
115 = Access (\val, p => ltAccessible' k (lteTransitive p x))
120 = Access (\val, p => ltAccessible' k (lteTransitive p x))
122+||| Strong induction principle for sized types.
117sizeInd : Sized a
123sizeInd : Sized a
118 => {P : a -> Type}
124 => {P : a -> Type}
119 -> (step : (x : a) -> ((y : a) -> Smaller y x -> P y) -> P x)
125 -> (step : (x : a) -> ((y : a) -> Smaller y x -> P y) -> P x)
@@ -121,6 +127,7 @@ sizeInd : Sized a
122sizeInd step z = accInd step z (accessible z)
128sizeInd step z = accInd step z (accessible z)
130+||| Strong recursion principle for sized types.
124sizeRec : Sized a
131sizeRec : Sized a
125 => (step : (x : a) -> ((y : a) -> Smaller y x -> b) -> b)
132 => (step : (x : a) -> ((y : a) -> Smaller y x -> b) -> b)
126 -> (z : a)
133 -> (z : a)