From aa6cdbb5747994db0abbc106ed325bd176f080a1 Mon Sep 17 00:00:00 2001 From: coquand Date: Fri, 3 Jul 2015 13:28:57 +0200 Subject: [PATCH] removed some examples (to be updated) --- examples/booltest.ctt | 32 ----------------------- examples/list.ctt | 3 +++ {examples => experiments}/deppath.ctt | 0 {examples => experiments}/exchange.ctt | 0 {examples => experiments}/helix.ctt | 0 {examples => experiments}/hopf.ctt | 0 {examples => experiments}/join.ctt | 0 {examples => experiments}/mystery.ctt | 0 {examples => experiments}/other.ctt | 0 {examples => experiments}/pi1S2output.ctt | 0 {examples => experiments}/pi1s2.ctt | 0 {examples => experiments}/pi4s3.ctt | 0 {examples => experiments}/pointed.ctt | 0 {examples => experiments}/s2.ctt | 0 {examples => experiments}/set.ctt | 0 {examples => experiments}/setTrunc.ctt | 0 {examples => experiments}/testall.ctt | 0 {examples => experiments}/thm7312.ctt | 0 {examples => experiments}/torus.ctt | 0 {examples => experiments}/truncS2.ctt | 0 {examples => experiments}/uafunext1.ctt | 0 {examples => experiments}/uafunext2.ctt | 0 22 files changed, 3 insertions(+), 32 deletions(-) delete mode 100644 examples/booltest.ctt rename {examples => experiments}/deppath.ctt (100%) rename {examples => experiments}/exchange.ctt (100%) rename {examples => experiments}/helix.ctt (100%) rename {examples => experiments}/hopf.ctt (100%) rename {examples => experiments}/join.ctt (100%) rename {examples => experiments}/mystery.ctt (100%) rename {examples => experiments}/other.ctt (100%) rename {examples => experiments}/pi1S2output.ctt (100%) rename {examples => experiments}/pi1s2.ctt (100%) rename {examples => experiments}/pi4s3.ctt (100%) rename {examples => experiments}/pointed.ctt (100%) rename {examples => experiments}/s2.ctt (100%) rename {examples => experiments}/set.ctt (100%) rename {examples => experiments}/setTrunc.ctt (100%) rename {examples => experiments}/testall.ctt (100%) rename {examples => experiments}/thm7312.ctt (100%) rename {examples => experiments}/torus.ctt (100%) rename {examples => experiments}/truncS2.ctt (100%) rename {examples => experiments}/uafunext1.ctt (100%) rename {examples => experiments}/uafunext2.ctt (100%) 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 -- 2.34.1