Mercurial > hg > Members > atton > agda-proofs
annotate sandbox/TypeClass.agda @ 41:2abf1cd97f10
Trying define type composition using list of subtype
author | atton <atton@cr.ie.u-ryukyu.ac.jp> |
---|---|
date | Tue, 03 Jan 2017 08:21:25 +0000 |
parents | e8494d175afb |
children |
rev | line source |
---|---|
5
e8494d175afb
Add sample for type class in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
1 -- type class example |
e8494d175afb
Add sample for type class in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
2 -- http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.InstanceArguments?from=ReferenceManual.Non-canonicalImplicitArguments |
e8494d175afb
Add sample for type class in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
3 |
e8494d175afb
Add sample for type class in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
4 open import Function |
e8494d175afb
Add sample for type class in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
5 open import Data.Bool |
e8494d175afb
Add sample for type class in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
6 open import Data.Nat |
e8494d175afb
Add sample for type class in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
7 |
e8494d175afb
Add sample for type class in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
8 record Eq (t : Set) : Set where |
e8494d175afb
Add sample for type class in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
9 field _==_ : t → t → Bool |
e8494d175afb
Add sample for type class in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
10 _/=_ : t → t → Bool |
e8494d175afb
Add sample for type class in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
11 a /= b = not $ a == b |
e8494d175afb
Add sample for type class in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
12 |
e8494d175afb
Add sample for type class in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
13 |
e8494d175afb
Add sample for type class in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
14 open module EqWithImplicits {t : Set} {{eqT : Eq t}} = Eq eqT |
e8494d175afb
Add sample for type class in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
15 |
e8494d175afb
Add sample for type class in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
16 instance |
e8494d175afb
Add sample for type class in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
17 postulate |
e8494d175afb
Add sample for type class in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
18 eqℕ : Eq ℕ |
e8494d175afb
Add sample for type class in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
19 eqBool : Eq Bool |
e8494d175afb
Add sample for type class in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
20 |
e8494d175afb
Add sample for type class in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
21 |
e8494d175afb
Add sample for type class in Agda
Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
22 test = 5 == 3 ∧ true /= false |