@@ -3,7 +3,7 @@
33||| This is to let us implement some functions that don't have trivial
44||| recursion patterns over datatypes, but instead are using some
55||| other metric of size.
6−module Control.WellFounded
6+module Prelude.WellFounded
77
88%default total
99%access public export
@@ -56,8 +56,8 @@ accRec step z (Access f) =
5656accInd : {rel : a -> a -> Type} -> {P : a -> Type} ->
5757 (step : (x : a) -> ((y : a) -> rel y x -> P y) -> P x) ->
5858 (z : a) -> Accessible rel z -> P z
59−accInd step z (Access f) =
60− step z $ \y, lt => accInd step y (f y lt)
59+accInd {P} step z (Access f) =
60+ step z $ \y, lt => accInd {P} step y (f y lt)
6161
6262
6363||| Use well-foundedness of a relation to write terminating operations.