idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-09-11 13:36:08 +03:00
Code Issues Projects Releases Wiki Activity

[ minor ] Remove a compilation warning from prelude

Browse Source
This commit is contained in:
Denis Buzdalov 2023-12-08 17:33:55 +03:00 committed by G. Allais
parent aa18be645d
commit e3ff0b7786
1 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
libs/prelude/Prelude/Basics.idr
View File

@ -126,9 +126,9 @@ public export
depCong2 : {0 p : a -> Type} ->
{0 q : (x : a) -> (y : p x) -> Type} ->
(0 f : (x : a) -> (y : p x) -> q x y) ->
{0 x1, x2 : a} -> (prf : x1 = x2) ->
{0 x1, x2 : a} -> (prfX : x1 = x2) ->
{0 y1 : p x1} -> {y2 : p x2} ->
(prf : y1 = y2) -> f x1 y1 = f x2 y2
(prfY : y1 = y2) -> f x1 y1 = f x2 y2
depCong2 f Refl Refl = Refl
||| Irrelevant equalities can always be made relevant