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

erase function argument of cong

Browse Source
This commit is contained in:
Alex Gryzlov 2020-05-24 05:16:52 +02:00
parent cf7de2201f
commit 723f690f7e
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
libs/prelude/Prelude.idr
View File

@ -117,7 +117,7 @@ public export
||| Equality is a congruence.
public export
cong : (f : t -> u) -> (1 p : a = b) -> f a = f b
cong : (0 f : t -> u) -> (1 p : a = b) -> f a = f b
cong f Refl = Refl
||| A canonical proof that some type is empty.