From 357a082a18bf1923d7b810349a36379fb18972a4 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Anders=20M=C3=B6rtberg?= Date: Tue, 5 May 2015 02:43:47 +0200 Subject: [PATCH] Swap test2 and test3 to correspond to what is in cubical --- examples/pi1S2.ctt | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/examples/pi1S2.ctt b/examples/pi1S2.ctt index 561f9e3..0d827ab 100644 --- a/examples/pi1S2.ctt +++ b/examples/pi1S2.ctt @@ -39,6 +39,7 @@ meridSstwo : Id stwo north south = merid{stwo} south@i trivstwo : pi1stwo = inc (refl stwo north) loopstwo : pi1stwo = inc (compId stwo north south north meridNstwo (meridSstwo@-i)) +test2 : Id pi1stwo trivstwo trivstwo = propPi1stwo trivstwo trivstwo + +test3 : Id pi1stwo trivstwo loopstwo = propPi1stwo trivstwo loopstwo -test2 : Id pi1stwo trivstwo loopstwo = propPi1stwo trivstwo loopstwo -test3 : Id pi1stwo trivstwo trivstwo = propPi1stwo trivstwo trivstwo -- 2.34.1