From d2cd0444d0cc5349fdf42892e644de7ab17cee81 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Anders=20M=C3=B6rtberg?= Date: Thu, 19 Apr 2018 10:00:18 -0400 Subject: [PATCH] add 5th winding number --- examples/circle.ctt | 1 + 1 file changed, 1 insertion(+) diff --git a/examples/circle.ctt b/examples/circle.ctt index 6254432..30a8d3b 100644 --- a/examples/circle.ctt +++ b/examples/circle.ctt @@ -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 -- 2.34.1