Source

pygments-main / tests / examplefiles / test.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; [_])

open SemiringSolver

{- this is a {- nested -} comment -}

-- 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 : (123 ∷ []) ++' (45 ∷ [])(12345 ∷ [])
++'-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
Tip: Filter by directory path e.g. /media app.js to search for public/media/app.js.
Tip: Use camelCasing e.g. ProjME to search for ProjectModifiedEvent.java.
Tip: Filter by extension type e.g. /repo .js to search for all .js files in the /repo directory.
Tip: Separate your search with spaces e.g. /ssh pom.xml to search for src/ssh/pom.xml.
Tip: Use ↑ and ↓ arrow keys to navigate and return to view the file.
Tip: You can also navigate files with Ctrl+j (next) and Ctrl+k (previous) and view the file with Ctrl+o.
Tip: You can also navigate files with Alt+j (next) and Alt+k (previous) and view the file with Alt+o.