Skip to content

Commit 192e6de

Browse files
committed
[fix] incorrect name for dependent chart constructor
1 parent 246053a commit 192e6de

File tree

1 file changed

+2
-2
lines changed

1 file changed

+2
-2
lines changed

src/Data/Container/Morphism/Definition.idr

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -54,8 +54,8 @@ namespace DependentCharts
5454
%name (=&>) f, g, h
5555

5656
public export
57-
(%!) : c1 =&> c2 -> (x : c1.Shp) -> (y : c2.Shp ** (c1.Pos x -> c2.Pos y))
58-
(%!) (!& f) x = f x
57+
(&!) : c1 =&> c2 -> (x : c1.Shp) -> (y : c2.Shp ** (c1.Pos x -> c2.Pos y))
58+
(&!) (!& f) x = f x
5959

6060
public export
6161
compDepChart : a =&> b -> b =&> c -> a =&> c

0 commit comments

Comments
 (0)