From 0727fa837d9361984299604c87003af0285c1fe1 Mon Sep 17 00:00:00 2001
From: Julin S <famubu@rawtext.club>
Date: Thu, 29 Feb 2024 23:24:14 +0530
Subject: [PATCH] [agda] add an example of using record type

---
 agda/pair-record.agda | 64 +++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 64 insertions(+)
 create mode 100644 agda/pair-record.agda

diff --git a/agda/pair-record.agda b/agda/pair-record.agda
new file mode 100644
index 0000000..652570c
--- /dev/null
+++ b/agda/pair-record.agda
@@ -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