110 lines
2.8 KiB
Agda
110 lines
2.8 KiB
Agda
-- 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
|