minor changes

diff --git a/examples/binnat.ctt b/examples/binnat.ctt
index d178d94bb686f69e912ed08896ed543db5f07a49..e9dca3a5b0a4ae6b99d09933710327a928e41827 100644 (file)
--- a/examples/binnat.ctt
+++ b/examples/binnat.ctt
@@ -153,7 +153,9 @@ elt : (D : Double) -> carrier D = split D _ _ e -> e
 
 DoubleN : Double = D nat doubleN n1024
 
-DoubleBinN : Double = D binN doubleBinN (NtoBinN n1024)
+bin1024 : binN = binNpos (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 (x0 pos1))))))))))
+
+DoubleBinN : Double = D binN doubleBinN bin1024
 
 -- iterate
 iter (A : U) : nat -> (A -> A) -> A -> A = split
@@ -162,10 +164,14 @@ iter (A : U) : nat -> (A -> A) -> A -> A = split
 
 ten : nat = add five five
 
--- 2^10 * e = 2^5 * (2^5 * e)
+-- Compute: 2^n * x
+doubles (D : Double) (n : nat) (x : carrier D) : carrier D = 
+  iter (carrier D) n (double D) x
+  
+-- 2^20 * e = 2^5 * (2^15 * e)
 propDouble (D : Double) : U
- = Path (carrier D) (iter (carrier D) ten (double D) (elt D))
-                              (iter (carrier D) five (double D) (iter (carrier D) five (double D) (elt D)))
+ = Path (carrier D) (doubles D n20 (elt D))
+                    (doubles D n5 (doubles D n15 (elt D)))
 
 -- The property we want to prove that takes long to typecheck:
 -- 2^10 * 1024 = 2^5 * (2^5 * 1024)
@@ -173,8 +179,7 @@ propDouble (D : Double) : U
 -- propN = refl N (doublesN ten n1024)
 
 -- With binary numbers it is instant
-propBin : propDouble DoubleBinN
- = <_> doublesBinN ten (elt DoubleBinN)
+propBin : propDouble DoubleBinN = <_> doublesBinN n20 (elt DoubleBinN)
 
 -- Define intermediate structure:
 doubleBinN' (b:binN) : binN = NtoBinN (doubleN (BinNtoN b))
@@ -200,11 +205,14 @@ eqDouble2 : Path Double DoubleBinN' DoubleBinN
                           [ (i=0) -> <_> NtoBinN (doubleN (PosToN p))
                           , (i=1) -> lem1 (x0 p) ]
 
-eqDouble : Path Double DoubleN DoubleBinN
- = compPath Double DoubleN DoubleBinN' DoubleBinN eqDouble1 eqDouble2
+eqDouble : Path Double DoubleN DoubleBinN =
+  compPath Double DoubleN DoubleBinN' DoubleBinN eqDouble1 eqDouble2
 
 opaque doubleN
 
-goal : propDouble DoubleN =
-  substInv Double propDouble DoubleN DoubleBinN eqDouble propBin
+propDoubleImpl : propDouble DoubleBinN -> propDouble DoubleN =
+  substInv Double propDouble DoubleN DoubleBinN eqDouble
+
+goal : propDouble DoubleN = propDoubleImpl propBin
 
+transparent_all
\ No newline at end of file

diff --git a/examples/nat.ctt b/examples/nat.ctt
index dadb9849d28eb19d94c329a627152fda94d93a2b..10baab4d0486193bd479f3e328bde55b86d7ce37 100644 (file)
--- a/examples/nat.ctt
+++ b/examples/nat.ctt
@@ -10,6 +10,28 @@ three : nat = suc two
 four : nat  = suc three
 five : nat  = suc four
 
+n0 : nat = zero
+n1 : nat = suc n0
+n2 : nat = suc n1
+n3 : nat = suc n2
+n4 : nat = suc n3
+n5 : nat = suc n4
+n6 : nat = suc n5
+n7 : nat = suc n6
+n8 : nat = suc n7
+n9 : nat = suc n8
+n10 : nat = suc n9
+n11 : nat = suc n10
+n12 : nat = suc n11
+n13 : nat = suc n12
+n14 : nat = suc n13
+n15 : nat = suc n14
+n16 : nat = suc n15
+n17 : nat = suc n16
+n18 : nat = suc n17
+n19 : nat = suc n18
+n20 : nat = suc n19
+
 pred : nat -> nat = split
   zero -> zero
   suc n -> n

diff --git a/examples/setquot.ctt b/examples/setquot.ctt
index 24dbafd7b9e25e3f98339e030cd3b467cb812c10..11ad02e6006d401bfaa865e1f7be8207b67a1516 100644 (file)
--- a/examples/setquot.ctt
+++ b/examples/setquot.ctt
@@ -86,8 +86,7 @@ sethProp (P P' : hProp) : prop (Path hProp P P') =
 
 hsubtypes (X : U) : U = X -> hProp
 
-carrier (X : U) (A : hsubtypes X) : U = Sigma X (\(x : X) -> (A x).1)
-
+carrier (X : U) (A : hsubtypes X) : U = (x : X) * (A x).1
 sethsubtypes (X : U) : set (hsubtypes X) =
   setPi X (\(_ : X) -> hProp) (\(_ : X) -> sethProp)