git.iko.soy/Idris-dev
on master help sign in
Make Iso a record
1c0bf46howtonotwin
libs/base/Control/Isomorphism.idr+6−6
compare with master
unifiedsplit
@@ -8,12 +8,12 @@ import Control.Category
8%access public export
8%access public export
9
9
10||| An isomorphism between two types
10||| An isomorphism between two types
11−data Iso : Type -> Type -> Type where
11+record Iso a b where
12+ constructor MkIso
12− MkIso : (to : a -> b) ->
13+ to : a -> b
13− (from : b -> a) ->
14+ from : b -> a
14− (toFrom : (y : b) -> to (from y) = y) ->
15+ toFrom : (y : b) -> to (from y) = y
15− (fromTo : (x : a) -> from (to x) = x) ->
16+ fromTo : (x : a) -> from (to x) = x
16− Iso a b
17
17
18-- Isomorphism properties
18-- Isomorphism properties
19
19
test/disambig002/disambig002.idr−5
@@ -19,11 +19,6 @@ Unique0 = Unique
19Unique1 : (t0 -> Type) -> Type
19Unique1 : (t0 -> Type) -> Type
20Unique1 {t0} t1 = (v : t0) -> Unique0 (t1 v)
20Unique1 {t0} t1 = (v : t0) -> Unique0 (t1 v)
21
21
22−namespace Iso
23−
24− from : {A, B : Type} -> Iso A B -> (B -> A)
25− from (MkIso to from toFrom fromTo) = from
26−
27namespace Fin
22namespace Fin
28
23
29 ||| 'Tail' of a finite function
24 ||| 'Tail' of a finite function