[agda] add an example of using record type
This commit is contained in:
parent
7129e29061
commit
0727fa837d
|
@ -0,0 +1,64 @@
|
||||||
|
module pair-record where
|
||||||
|
-- https://agda.readthedocs.io/en/latest/language/record-types.html
|
||||||
|
|
||||||
|
open import Data.Nat using (ℕ; _+_)
|
||||||
|
|
||||||
|
|
||||||
|
record Pair (A B : Set) : Set where
|
||||||
|
field
|
||||||
|
fst : A
|
||||||
|
snd : A
|
||||||
|
|
||||||
|
getA : {A B : Set} -> Pair A B -> A
|
||||||
|
getA p = Pair.fst p
|
||||||
|
|
||||||
|
getB : {A B : Set} -> Pair A B -> A
|
||||||
|
getB = Pair.snd
|
||||||
|
|
||||||
|
|
||||||
|
-- Record expression
|
||||||
|
eg1 : Pair ℕ ℕ
|
||||||
|
eg1 = record { fst = 2; snd = 3 }
|
||||||
|
|
||||||
|
-- λ> getA eg1
|
||||||
|
-- 2
|
||||||
|
|
||||||
|
|
||||||
|
-- Co-patterns (prefix)
|
||||||
|
eg2 : Pair ℕ ℕ
|
||||||
|
Pair.fst eg2 = 4
|
||||||
|
Pair.snd eg2 = 6
|
||||||
|
|
||||||
|
-- λ> getB eg2
|
||||||
|
-- 6
|
||||||
|
|
||||||
|
-- Co-patterns (suffix)
|
||||||
|
eg3 : Pair ℕ ℕ
|
||||||
|
eg3 .Pair.fst = 8
|
||||||
|
eg3 .Pair.snd = 12
|
||||||
|
|
||||||
|
-- Anon co-pattern matching lambda
|
||||||
|
eg4 : Pair ℕ ℕ
|
||||||
|
eg4 = λ where
|
||||||
|
.Pair.fst -> 8
|
||||||
|
.Pair.snd -> 12
|
||||||
|
|
||||||
|
----------------------------------------------------------
|
||||||
|
|
||||||
|
-- If `constructor' was used in the record definition,
|
||||||
|
-- we can use that as a notation
|
||||||
|
|
||||||
|
record Pair2 (A B : Set) : Set where
|
||||||
|
constructor _,_ -- This will become a notation
|
||||||
|
field
|
||||||
|
fst2 : A
|
||||||
|
snd2 : B
|
||||||
|
|
||||||
|
getA2 : {A B : Set} -> Pair2 A B -> A
|
||||||
|
getA2 = Pair2.fst2
|
||||||
|
|
||||||
|
eg5 : Pair2 ℕ ℕ
|
||||||
|
eg5 = 2 , 3
|
||||||
|
|
||||||
|
-- λ> getA2 eg5
|
||||||
|
-- 2
|
Loading…
Reference in New Issue