idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-19 01:01:59 +03:00
Code Issues Projects Releases Wiki Activity

Add dependent congruence of arity 1 and 2 for heterogeneous equality

Browse Source
This commit is contained in:
russoul 2022-05-06 01:01:49 +04:00 committed by G. Allais
parent 82e4fd9da7
commit f2e6dc4313
1 changed files with 19 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -112,6 +112,25 @@ export
cong2 : (0 f : t1 -> t2 -> u) -> (0 p1 : a = b) -> (0 p2 : c = d) -> f a c = f b d cong2 : (0 f : t1 -> t2 -> u) -> (0 p1 : a = b) -> (0 p2 : c = d) -> f a c = f b d
cong2 f Refl Refl = Refl cong2 f Refl Refl = Refl
||| Dependent version of `cong`.
public export
depCong : {0 p : a -> Type} ->
(0 f : (x : a) -> p x) ->
{0 x1, x2 : a} ->
(prf : x1 = x2) ->
f x1 = f x2
depCong f Refl = Refl
||| Dependent version of `cong2`.
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 y1 : p x1} -> {y2 : p x2} ->
(prf : y1 = y2) -> f x1 y1 = f x2 y2
depCong2 f Refl Refl = Refl
||| Irrelevant equalities can always be made relevant ||| Irrelevant equalities can always be made relevant
export export
irrelevantEq : (0 _ : a ~=~ b) -> a ~=~ b irrelevantEq : (0 _ : a ~=~ b) -> a ~=~ b