Skip to content

Commit

Permalink
add 5th winding number
Browse files Browse the repository at this point in the history
  • Loading branch information
@mortberg
mortberg committed Apr 19, 2018
1 parent bf8253f commit d2cd044
Showing 1 changed file with 1 addition and 0 deletions.
1 change: 1 addition & 0 deletions examples/circle.ctt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -39,6 +39,7 @@ loopZ2 : Z = winding (compS1 loop1 loop1)
loopZ3 : Z = winding (compS1 loop1 (compS1 loop1 loop1))
loopZN1 : Z = winding invLoop
loopZ0 : Z = winding (compS1 loop1 invLoop)
loopZ5 : Z = winding (compS1 loop1 (compS1 loop1 (compS1 loop1 (compS1 loop1 loop1))))

mLoop : (x : S1) -> Path S1 x x = split
base -> loop1
Expand Down

0 comments on commit d2cd044

Please sign in to comment.