blob: f6cea91c6de99f4a7613bea9700432a4fc320cbc (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
|
-- 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
|
