annotate sandbox/TypeClass.agda @ 77:a2e6f61d5f2b default tip

Add modus-ponens
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Thu, 09 Feb 2017 06:32:03 +0000
parents e8494d175afb
children
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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