65 lines
1.1 KiB
Agda
65 lines
1.1 KiB
Agda
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
|