Remove all files, redirect to GitHub.HEADmaster

1 files changed, 0 insertions, 109 deletions

diff --git a/tests/examplefiles/test.agda b/tests/examplefiles/test.agda
deleted file mode 100644
index f6cea91c..00000000
--- a/tests/examplefiles/test.agda
+++ /dev/null
@@ -1,109 +0,0 @@
--- An Agda example file
-
-module test where
-
-open import Coinduction
-open import Data.Bool
-open import {- pointless comment between import and module name -} Data.Char
-open import Data.Nat
-open import Data.Nat.Properties
-open import Data.String
-open import Data.List hiding ([_])
-open import Data.Vec hiding ([_])
-open import Relation.Nullary.Core
-open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; trans; inspect; [_])
-  renaming (setoid to setiod)
-
-open SemiringSolver
-
-{- this is a {- nested -} comment -}
-
-postulate pierce : {A B : Set} → ((A → B) → A) → A
-
-instance
-  someBool : Bool
-  someBool = true
-
--- Factorial
-_! : ℕ → ℕ
-0 ! = 1
-(suc n) ! = (suc n) * n !
-
--- The binomial coefficient
-_choose_ : ℕ → ℕ → ℕ
-_ choose 0 = 1
-0 choose _ = 0
-(suc n) choose (suc m) = (n choose m) + (n choose (suc m)) -- Pascal's rule
-
-choose-too-many : ∀ n m → n ≤ m → n choose (suc m) ≡ 0
-choose-too-many .0 m z≤n = refl
-choose-too-many (suc n) (suc m) (s≤s le) with n choose (suc m) | choose-too-many n m le | n choose (suc (suc m)) | choose-too-many n (suc m) (≤-step le)
-... | .0 | refl | .0 | refl = refl
-
-_++'_ : ∀ {a n m} {A : Set a} → Vec A n → Vec A m → Vec A (m + n)
-_++'_ {_} {n} {m} v₁ v₂ rewrite solve 2 (λ a b → b :+ a := a :+ b) refl n m = v₁ Data.Vec.++ v₂
-
-++'-test : (1 ∷ 2 ∷ 3 ∷ []) ++' (4 ∷ 5 ∷ []) ≡ (1 ∷ 2 ∷ 3 ∷ 4 ∷ 5 ∷ [])
-++'-test = refl
-
-data Coℕ : Set where
-  co0   : Coℕ
-  cosuc : ∞ Coℕ → Coℕ
-
-nanana : Coℕ
-nanana = let two = ♯ cosuc (♯ (cosuc (♯ co0))) in cosuc two
-
-abstract
-  data VacuumCleaner : Set where
-    Roomba : VacuumCleaner
-
-pointlessLemmaAboutBoolFunctions : (f : Bool → Bool) → f (f (f true)) ≡ f true
-pointlessLemmaAboutBoolFunctions f with f true | inspect f true
-... | true  | [ eq₁ ] = trans (cong f eq₁) eq₁
-... | false | [ eq₁ ] with f false | inspect f false
-... | true  | _       = eq₁
-... | false | [ eq₂ ] = eq₂
-
-mutual
-  isEven : ℕ → Bool
-  isEven 0       = true
-  isEven (suc n) = not (isOdd n)
-
-  isOdd : ℕ → Bool
-  isOdd 0       = false
-  isOdd (suc n) = not (isEven n)
-
-foo : String
-foo = "Hello World!"
-
-nl : Char
-nl = '\n'
-
-private
-  intersperseString : Char → List String → String
-  intersperseString c []       = ""
-  intersperseString c (x ∷ xs) = Data.List.foldl (λ a b → a Data.String.++ Data.String.fromList (c ∷ []) Data.String.++ b) x xs
-
-baz : String
-baz = intersperseString nl (Data.List.replicate 5 foo)
-
-postulate
-  Float : Set
-
-{-# BUILTIN FLOAT Float  #-}
-
-pi : Float
-pi = 3.141593
-
--- Astronomical unit
-au : Float
-au = 1.496e11 -- m
-
-plusFloat : Float → Float → Float
-plusFloat a b = {! !}
-
-record Subset (A : Set) (P : A → Set) : Set where
-  constructor _#_
-  field
-    elem   : A
-    .proof : P elem