idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-11-20 17:18:26 +03:00
Code Issues Projects Releases Wiki Activity

Public export Decidable.Decidable.decision

Browse Source
This commit is contained in:
Michael Messer 2024-06-25 22:12:40 -05:00 committed by G. Allais
parent 7d33c0438a
commit 5f27842cbc
2 changed files with 3 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
CHANGELOG_NEXT.md
View File

@ -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`.

1
libs/base/Decidable/Decidable.idr
View File

@ -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}