mirror of
https://github.com/edwinb/Idris2-boot.git
synced 2024-12-24 21:34:36 +03:00
remove ide socket mode test because it's hard to make reliable
This commit is contained in:
parent
b682accc0b
commit
39a5c25fbc
@ -1 +0,0 @@
|
||||
module Empty
|
@ -1,34 +0,0 @@
|
||||
data Nat = Z | S Nat
|
||||
|
||||
plus : Nat -> Nat -> Nat
|
||||
plus Z y = y
|
||||
plus (S k) y = S (plus k y)
|
||||
|
||||
data Vect : Nat -> Type -> Type where
|
||||
Nil : Vect Z a
|
||||
Cons : a -> Vect k a -> Vect (S k) a
|
||||
|
||||
foldl : (0 b : Nat -> Type) ->
|
||||
({k : Nat} -> b k -> a -> b (S k)) ->
|
||||
b Z ->
|
||||
Vect n a -> b n
|
||||
foldl b g z Nil = z
|
||||
foldl b g z (Cons x xs) = foldl (\i => b (S i)) g (g z x) xs
|
||||
|
||||
reverse : Vect n a -> Vect n a
|
||||
reverse
|
||||
= foldl (\m => Vect m a)
|
||||
(\rev => \x => Cons x rev) Nil
|
||||
|
||||
append : Vect n a -> Vect m a -> Vect (plus n m) a
|
||||
append Nil ys = ys
|
||||
append (Cons x xs) ys = Cons x (append xs ys)
|
||||
|
||||
vlength : (n : Nat) -> Vect n a -> Nat
|
||||
vlength Z Nil = Z
|
||||
vlength n@_ (Cons x xs) = n -- (vlength _ xs);
|
||||
|
||||
zipWith : (a -> b -> c) -> Vect n a -> Vect n b -> Vect n c
|
||||
zipWith f Nil Nil = Nil
|
||||
-- zipWith f (Cons x xs) Nil impossible
|
||||
zipWith f (Cons x xs) (Cons y ys) = Cons (f x y) (zipWith f xs ys)
|
@ -1,3 +0,0 @@
|
||||
000018(:protocol-version 2 0)
|
||||
000032(:write-string "1/1: Building Vect (Vect.idr)" 1)
|
||||
000027(:return (:ok "Loaded Vect.idr" ()) 1)
|
@ -1 +0,0 @@
|
||||
00001b((:load-file "Vect.idr") 1)
|
@ -1,7 +0,0 @@
|
||||
$1 --no-prelude --ide-mode-socket 0.0.0.0:34567 Empty.idr > /dev/null &
|
||||
sleep 2
|
||||
|
||||
nc -G 5 127.0.0.1 34567 < input
|
||||
|
||||
kill %1
|
||||
rm -rf build
|
Loading…
Reference in New Issue
Block a user