From c02f09b14eb296dc984b52074841b09f8fffb984 Mon Sep 17 00:00:00 2001
From: =?utf8?q?Anders=20M=C3=B6rtberg?= <mortberg@chalmers.se>
Date: Mon, 13 Apr 2015 19:41:17 +0200
Subject: [PATCH] Move stream to experiments

---
 {examples => experiments}/stream.ctt | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)
 rename {examples => experiments}/stream.ctt (94%)

diff --git a/examples/stream.ctt b/experiments/stream.ctt
similarity index 94%
rename from examples/stream.ctt
rename to experiments/stream.ctt
index db05e08..e7f7c03 100644
--- a/examples/stream.ctt
+++ b/experiments/stream.ctt
@@ -1,6 +1,15 @@
 module stream where
 
-import prelude
+-- Things from the prelude:
+Id (A : U) (a0 a1 : A) : U = IdP (<i> A) a0 a1
+
+refl (A : U) (a : A) : Id A a a = <i> a
+
+isoId (A B : U) (f : A -> B) (g : B -> A)
+      (s : (y:B) -> Id B (f (g y)) y)
+      (t : (x:A) -> Id A (g (f x)) x) : Id U A B =
+      <i> glue B [ (i = 0) -> (A,f,g,s,t) ]
+
 
 -- Let us pretend that Stream is a coinductive type.
 
-- 
2.34.1