add list concat sample

newt/Prelude.newt

@@ -42,6 +42,14 @@ ma >> mb = mb
 pure : {a : U} {m : U -> U} {{_ : Monad m}} -> a -> m a
 pure {_} {_} {{MkMonad _ pure'}} a = pure' a
 
--- IO
+infixl 1 _≡_
+data _≡_ : {A : U} -> A -> A -> U where
+  Refl :  {A : U} -> {a : A} -> a ≡ a
 
+replace : {A : U} {a b : A} -> (P : A -> U) -> a ≡ b -> P a -> P b
+replace p Refl x = x
 
+cong : {A B : U} {a b : A} -> (f : A -> B) -> a ≡ b -> f a ≡ f b
+
+sym : {A : U} -> {a b : A} -> a ≡ b -> b ≡ a
+sym Refl = Refl

playground/samples/Concat.newt

@@ -0,0 +1,38 @@
+module Concat
+
+data Nat : U where
+    Z : Nat
+    S : Nat -> Nat
+
+infixl 7 _+_
+_+_ : Nat -> Nat -> Nat
+Z + m = m
+S n + m = S (n + m)
+
+infixr 3 _::_
+data List : U -> U where
+    Nil : {A : U} -> List A
+    _::_ : {A : U} -> A -> List A -> List A
+
+length : {A : U} -> List A -> Nat
+length Nil = Z
+length (x :: xs) = S (length xs)
+
+infixl 2 _++_
+
+_++_ : {A : U} -> List A -> List A -> List A
+Nil ++ ys = ys
+x :: xs ++ ys = x :: (xs ++ ys)
+
+infixl 1 _≡_
+data _≡_ : {A : U} -> A -> A -> U where
+    Refl : {A : U} {a : A} -> a ≡ a
+
+replace : {A : U} {a b : A} -> (P : A -> U) -> a ≡ b -> P a -> P b
+replace p Refl x = x
+
+cong : {A B : U} {a b : A} -> (f : A -> B) -> a ≡ b -> f a ≡ f b
+
+thm : {A : U} (xs ys : List A) -> length (xs ++ ys) ≡ length xs + length ys
+thm Nil ys = Refl
+thm (x :: xs) ys = cong S (thm xs ys)

playground/src/main.ts

@@ -145,9 +145,10 @@ const SAMPLES = [
   "Tour.newt",
   "Tree.newt",
   // "Prelude.newt",
-  "Lib.newt",
+  "Concat.newt",
   "Day1.newt",
   "Day2.newt",
+  "Lib.newt",
   "TypeClass.newt",
 ];
 

tests/black/Concat.newt

@@ -0,0 +1,38 @@
+module Concat
+
+data Nat : U where
+    Z : Nat
+    S : Nat -> Nat
+
+infixl 7 _+_
+_+_ : Nat -> Nat -> Nat
+Z + m = m
+S n + m = S (n + m)
+
+infixr 3 _::_
+data List : U -> U where
+    Nil : {A : U} -> List A
+    _::_ : {A : U} -> A -> List A -> List A
+
+length : {A : U} -> List A -> Nat
+length Nil = Z
+length (x :: xs) = S (length xs)
+
+infixl 2 _++_
+
+_++_ : {A : U} -> List A -> List A -> List A
+Nil ++ ys = ys
+x :: xs ++ ys = x :: (xs ++ ys)
+
+infixl 1 _≡_
+data _≡_ : {A : U} -> A -> A -> U where
+    Refl : {A : U} {a : A} -> a ≡ a
+
+replace : {A : U} {a b : A} -> (P : A -> U) -> a ≡ b -> P a -> P b
+replace p Refl x = x
+
+cong : {A B : U} {a b : A} -> (f : A -> B) -> a ≡ b -> f a ≡ f b
+
+thm : {A : U} (xs ys : List A) -> length (xs ++ ys) ≡ length xs + length ys
+thm Nil ys = Refl
+thm (x :: xs) ys = cong S (thm xs ys)