From d83e672abd36013b3b920ff95cb2c12f1c1f224f Mon Sep 17 00:00:00 2001 From: =?utf8?q?Rafa=C3=ABl=20Bocquet?= Date: Thu, 14 Apr 2016 14:17:08 +0200 Subject: [PATCH] simple computation using multZ --- examples/torsor.ctt | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/examples/torsor.ctt b/examples/torsor.ctt index 2f2ad37..2983ab1 100644 --- a/examples/torsor.ctt +++ b/examples/torsor.ctt @@ -851,5 +851,11 @@ doubleLoopBZ : loopBZ -> loopBZ = transport ( loopS1equalsLoopBZ@i -> loopS1e -- Time: 0m25.191s -- > let visible_all in let doubleLoop : Id BZ (multZ ZBZ ZBZ) (multZ ZBZ ZBZ) = multZ (loopZ@-i) (loopZ@i) in transport ( BZSet (transport ( BZSet (doubleLoop @ i)) (<_> ZBZ) @ j)) zeroZ +-- too slow + +-- > let visible_all in transport ( BZSet (transport ( BZSet (multZ (loopZ@-i) (loopZ@i))) (<_> ZBZ) @ j)) zeroZ +-- EVAL: inr (suc (suc zero)) + +-- multS1 : S1 -> S1 -> S1 = transport ( S1equalsBZ@-i -> S1equalsBZ@-i -> S1equalsBZ@-i) multZ visible_all -- 2.34.1