@@ -86,14 +86,19 @@ wfInd : WellFounded rel => {P : a -> Type} ->
8686wfInd {rel} step x = accInd step x (wellFounded {rel} x)
8787
8888
89−-- Accessibility for sized types
90−
89+||| Interface of types with sized values.
90+|||
91+||| The sizes are used for proofs of termination via accessibility.
92+|||
93+||| @ a the type whose elements can be mapped to Nat
9194interface Sized a where
9295 size : a -> Nat
9396
9497Smaller : Sized a => a -> a -> Type
9598Smaller x y = size x `LT` size y
9699
100+||| Proof of well-foundedness of `Smaller`.
101+||| Constructs accessibility for any given element of `a`, provided `Sized a`.
97102accessible : Sized a => (x : a) -> Accessible Smaller x
98103accessible x = Access $ f (size x) (ltAccessible $ size x)
99104 where
@@ -114,6 +119,7 @@ accessible x = Access $ f (size x) (ltAccessible $ size x)
114119 ltAccessible' (S k) (LTESucc x)
115120 = Access (\val, p => ltAccessible' k (lteTransitive p x))
116121
122+||| Strong induction principle for sized types.
117123sizeInd : Sized a
118124 => {P : a -> Type}
119125 -> (step : (x : a) -> ((y : a) -> Smaller y x -> P y) -> P x)
@@ -121,6 +127,7 @@ sizeInd : Sized a
121127 -> P z
122128sizeInd step z = accInd step z (accessible z)
123129
130+||| Strong recursion principle for sized types.
124131sizeRec : Sized a
125132 => (step : (x : a) -> ((y : a) -> Smaller y x -> b) -> b)
126133 -> (z : a)