git.iko.soy/Idris-dev
on master help sign in
Move Accessible to Prelude
87fb53aEdwin Brady
libs/contrib/Data/Nat/DivMod/IteratedSubtraction.idr−2
compare with master
unifiedsplit
@@ -5,8 +5,6 @@ module Data.Nat.DivMod.IteratedSubtraction
5import Data.Fin
5import Data.Fin
6import Data.So
6import Data.So
7
7
8−import Control.WellFounded
9−
10%default total
8%default total
11%access public export
9%access public export
12
10
libs/contrib/contrib.ipkg−1
@@ -8,7 +8,6 @@ modules = CFFI, CFFI.Types, CFFI.Memory,
8 Control.Algebra.NumericInstances,
8 Control.Algebra.NumericInstances,
9 Control.Isomorphism.Primitives,
9 Control.Isomorphism.Primitives,
10 Control.Partial,
10 Control.Partial,
11− Control.WellFounded,
12
11
13 Classes.Verified,
12 Classes.Verified,
14
13
libs/prelude/Prelude.idr+1
@@ -28,6 +28,7 @@ import public Prelude.Show
28import public Prelude.Interactive
28import public Prelude.Interactive
29import public Prelude.File
29import public Prelude.File
30import public Prelude.Doubles
30import public Prelude.Doubles
31+import public Prelude.WellFounded
31import public Decidable.Equality
32import public Decidable.Equality
32import public Language.Reflection
33import public Language.Reflection
33import public Language.Reflection.Elab
34import public Language.Reflection.Elab
libs/contrib/Control/WellFounded.idr → libs/prelude/Prelude/WellFounded.idrrenamed+3−3
@@ -3,7 +3,7 @@
3||| This is to let us implement some functions that don't have trivial
3||| This is to let us implement some functions that don't have trivial
4||| recursion patterns over datatypes, but instead are using some
4||| recursion patterns over datatypes, but instead are using some
5||| other metric of size.
5||| other metric of size.
6−module Control.WellFounded
6+module Prelude.WellFounded
7
7
8%default total
8%default total
9%access public export
9%access public export
@@ -56,8 +56,8 @@ accRec step z (Access f) =
56accInd : {rel : a -> a -> Type} -> {P : a -> Type} ->
56accInd : {rel : a -> a -> Type} -> {P : a -> Type} ->
57 (step : (x : a) -> ((y : a) -> rel y x -> P y) -> P x) ->
57 (step : (x : a) -> ((y : a) -> rel y x -> P y) -> P x) ->
58 (z : a) -> Accessible rel z -> P z
58 (z : a) -> Accessible rel z -> P z
59−accInd step z (Access f) =
59+accInd {P} step z (Access f) =
60− step z $ \y, lt => accInd step y (f y lt)
60+ step z $ \y, lt => accInd {P} step y (f y lt)
61
61
62
62
63||| Use well-foundedness of a relation to write terminating operations.
63||| Use well-foundedness of a relation to write terminating operations.
libs/prelude/prelude.ipkg+1
@@ -10,6 +10,7 @@ modules = Builtins, Prelude, IO,
10 Prelude.Foldable, Prelude.Traversable, Prelude.Bits, Prelude.Stream,
10 Prelude.Foldable, Prelude.Traversable, Prelude.Bits, Prelude.Stream,
11 Prelude.Uninhabited, Prelude.Pairs, Prelude.Providers,
11 Prelude.Uninhabited, Prelude.Pairs, Prelude.Providers,
12 Prelude.Interactive, Prelude.File, Prelude.Doubles,
12 Prelude.Interactive, Prelude.File, Prelude.Doubles,
13+ Prelude.WellFounded,
13
14
14 Language.Reflection, Language.Reflection.Errors, Language.Reflection.Elab,
15 Language.Reflection, Language.Reflection.Errors, Language.Reflection.Elab,
15
16