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

[ refactor ] renamed value to runConst

Browse Source
This commit is contained in:
stefan-hoeck 2021-04-25 10:30:52 +02:00 committed by G. Allais
parent 7863636490
commit 0858c26dcf
1 changed files with 3 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
libs/base/Control/Applicative/Const.idr
View File

@ -6,15 +6,15 @@ import Data.Bits
public export
record Const (a : Type) (b : Type) where
constructor MkConst
value : a
runConst : a
public export
Eq a => Eq (Const a b) where
(==) = (==) `on` value
(==) = (==) `on` runConst
public export
Ord a => Ord (Const a b) where
compare = compare `on` value
compare = compare `on` runConst
export
Show a => Show (Const a b) where