We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 192e6de commit c58b595Copy full SHA for c58b595
src/Data/Container/Morphism/Definition.idr
@@ -26,9 +26,12 @@ namespace DependentLenses
26
27
%name (=%>) f, g, h
28
29
+
30
+ public export prefix 0 %!
31
public export
32
(%!) : c1 =%> c2 -> (x : c1.Shp) -> (y : c2.Shp ** (c2.Pos y -> c1.Pos x))
33
(%!) (!% f) x = f x
34
35
36
||| Composition of dependent lenses
37
@@ -53,6 +56,7 @@ namespace DependentCharts
53
56
54
57
%name (=&>) f, g, h
55
58
59
+ public export prefix 0 &!
60
61
(&!) : c1 =&> c2 -> (x : c1.Shp) -> (y : c2.Shp ** (c1.Pos x -> c2.Pos y))
62
(&!) (!& f) x = f x
0 commit comments