From: coquand Date: Fri, 3 Jul 2015 11:28:57 +0000 (+0200) Subject: removed some examples (to be updated) X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=aa6cdbb5747994db0abbc106ed325bd176f080a1;p=cubicaltt.git removed some examples (to be updated) --- diff --git a/examples/booltest.ctt b/examples/booltest.ctt deleted file mode 100644 index 3d20e99..0000000 --- a/examples/booltest.ctt +++ /dev/null @@ -1,32 +0,0 @@ -module booltest where - -import bool -import newhedberg - -falseNotTrue (h : Id bool false true) : N0 = transport ( T (h @ i)) tt - where T : bool -> U = split - false -> Unit - true -> N0 - -trueNotFalse (h : Id bool true false) : N0 = falseNotTrue ( h @ - i) - -lemFalse : (b : bool) -> dec (Id bool false b) = split - false -> inl ( false) - true -> inr falseNotTrue - -lemTrue : (b : bool) -> dec (Id bool true b) = split - false -> inr trueNotFalse - true -> inl ( true) - -boolDec : (a b : bool) -> dec (Id bool a b) = split - false -> lemFalse - true -> lemTrue - -boolSet : set bool = corrhedberg bool boolDec - -F2Set : set F2 = subst U set bool F2 boolEqF2 boolSet - -T : U = Id F2 oneF2 oneF2 -p0 : T = refl F2 oneF2 - -test : Id T p0 p0 = F2Set oneF2 oneF2 p0 p0 \ No newline at end of file diff --git a/examples/list.ctt b/examples/list.ctt index da6b6ce..cba3326 100644 --- a/examples/list.ctt +++ b/examples/list.ctt @@ -39,6 +39,8 @@ assoc (A:U) : (xs ys zs : list A) -> Id (list A) (append A (append A xs ys) zs) nil -> \ (ys zs:list A) -> append A ys zs cons x xs -> \ (ys zs:list A) -> cons x (assoc A xs ys zs@i) +{- + lem4 (A:U) : (xs ys:list A) -> Id (list A) (reverse A (append A xs ys)) (append A (reverse A ys) (reverse A xs)) = split nil -> \ (ys:list A) -> lem2 A (reverse A ys)@-i cons x xs -> \ (ys:list A) -> comp (list A) (append A (lem4 A xs ys@i) (cons x nil)) @@ -48,3 +50,4 @@ lem5 (A:U) : (xs:list A) -> Id (list A) (reverse A (reverse A xs)) xs = split nil -> nil cons x xs -> comp (list A) (lem4 A (reverse A xs) (cons x nil)@i) [(i=1) -> cons x (lem5 A xs@j)] +-} diff --git a/examples/deppath.ctt b/experiments/deppath.ctt similarity index 100% rename from examples/deppath.ctt rename to experiments/deppath.ctt diff --git a/examples/exchange.ctt b/experiments/exchange.ctt similarity index 100% rename from examples/exchange.ctt rename to experiments/exchange.ctt diff --git a/examples/helix.ctt b/experiments/helix.ctt similarity index 100% rename from examples/helix.ctt rename to experiments/helix.ctt diff --git a/examples/hopf.ctt b/experiments/hopf.ctt similarity index 100% rename from examples/hopf.ctt rename to experiments/hopf.ctt diff --git a/examples/join.ctt b/experiments/join.ctt similarity index 100% rename from examples/join.ctt rename to experiments/join.ctt diff --git a/examples/mystery.ctt b/experiments/mystery.ctt similarity index 100% rename from examples/mystery.ctt rename to experiments/mystery.ctt diff --git a/examples/other.ctt b/experiments/other.ctt similarity index 100% rename from examples/other.ctt rename to experiments/other.ctt diff --git a/examples/pi1S2output.ctt b/experiments/pi1S2output.ctt similarity index 100% rename from examples/pi1S2output.ctt rename to experiments/pi1S2output.ctt diff --git a/examples/pi1s2.ctt b/experiments/pi1s2.ctt similarity index 100% rename from examples/pi1s2.ctt rename to experiments/pi1s2.ctt diff --git a/examples/pi4s3.ctt b/experiments/pi4s3.ctt similarity index 100% rename from examples/pi4s3.ctt rename to experiments/pi4s3.ctt diff --git a/examples/pointed.ctt b/experiments/pointed.ctt similarity index 100% rename from examples/pointed.ctt rename to experiments/pointed.ctt diff --git a/examples/s2.ctt b/experiments/s2.ctt similarity index 100% rename from examples/s2.ctt rename to experiments/s2.ctt diff --git a/examples/set.ctt b/experiments/set.ctt similarity index 100% rename from examples/set.ctt rename to experiments/set.ctt diff --git a/examples/setTrunc.ctt b/experiments/setTrunc.ctt similarity index 100% rename from examples/setTrunc.ctt rename to experiments/setTrunc.ctt diff --git a/examples/testall.ctt b/experiments/testall.ctt similarity index 100% rename from examples/testall.ctt rename to experiments/testall.ctt diff --git a/examples/thm7312.ctt b/experiments/thm7312.ctt similarity index 100% rename from examples/thm7312.ctt rename to experiments/thm7312.ctt diff --git a/examples/torus.ctt b/experiments/torus.ctt similarity index 100% rename from examples/torus.ctt rename to experiments/torus.ctt diff --git a/examples/truncS2.ctt b/experiments/truncS2.ctt similarity index 100% rename from examples/truncS2.ctt rename to experiments/truncS2.ctt diff --git a/examples/uafunext1.ctt b/experiments/uafunext1.ctt similarity index 100% rename from examples/uafunext1.ctt rename to experiments/uafunext1.ctt diff --git a/examples/uafunext2.ctt b/experiments/uafunext2.ctt similarity index 100% rename from examples/uafunext2.ctt rename to experiments/uafunext2.ctt