Public export Decidable.Decidable.decision

idris-lang · Jun 26, 2024 · 8dc0436 · 8dc0436
1 parent 7d33c04
commit 8dc0436
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 0 deletions.
diff --git a/CHANGELOG_NEXT.md b/CHANGELOG_NEXT.md
@@ -186,6 +186,8 @@ This CHANGELOG describes the merged but unreleased changes. Please see [CHANGELO
 * Some pieces of `Data.Fin.Extra` from `contrib` were moved to `base` to modules
   `Data.Fin.Properties`, `Data.Fin.Arith` and `Data.Fin.Split`.
 
+* `Decidable.Decidable.decison` is now `public export`.
+
 #### Contrib
 
 * `Data.List.Lazy` was moved from `contrib` to `base`.

diff --git a/libs/base/Decidable/Decidable.idr b/libs/base/Decidable/Decidable.idr
@@ -51,5 +51,6 @@ interface Decidable k ts p where
 
 ||| Given a `Decidable` n-ary relation, provides a decision procedure for
 ||| this relation.
+public export
 decision : (ts : Vect k Type) -> (p : Rel ts) -> Decidable k ts p => liftRel ts p Dec
 decision ts p = decide {ts} {p}