:PROPERTIES:
:ID:       f6c9e1a7-8465-4cef-9481-2b803d0c43d4
:END:
#+title: afp_lab_1
#+filetags: :notes:uni:
<2025-01-20 Mon> 
* Installation of Agda:
** Step 1
#+BEGIN_SRC eshell
sudo apt-get install zlib1g-dev libncurses5-dev
#+END_SRC

then install ghc
- https://www.haskell.org/ghcup/

Now that you have cabal installed, use it to install Agda as a Haskell package:
#+BEGIN_SRC eshell
cabal update
cabal install Agda
#+END_SRC
** Step 2
Most users will want to install the standard library. You can install this as any other Agda library (see Library Management). See the agda-stdlib project’s installation instructions for the steps to take to install the latest version.
https://github.com/agda/agda-stdlib
https://agda.readthedocs.io/en/latest/tools/package-system.html#package-system
* Exercises:
[[file:~/master-folder/Uni/ADVFUNC/afp-learning-2024-2025/files/LectureNotes/files/exercises/my-lab1.lagda.md][my lab1]]


```agda
data Bool : Type where
 true false : Bool
```

 
In Agda, the snippet `data Bool : Type where true false : Bool` is a definition of a simple data type named `Bool`. Let’s break down and explain all the components and words in this snippet:

---

### 1. **`data`**
- **What it means:** This keyword introduces a new *data type* definition in Agda.
- **Purpose:** Defines a type that consists of one or more *constructors*, which are used to create values of the type.
- **In this case:** The `data` keyword is used to define the `Bool` type.

---

### 2. **`Bool`**
- **What it is:** The name of the data type being defined.
- **Purpose:** Represents a type that has exactly two possible values: `true` and `false`.
- **In this case:** `Bool` is a common type used to represent truth values in logic (true or false).

---

### 3. **`:` (colon)**
- **What it means:** Indicates a type declaration in Agda.
- **Purpose:** Separates the name of the data type (`Bool`) from its type (`Type`).
- **In this case:** `Bool : Type` declares that `Bool` is a type itself (i.e., a type of values).

---

### 4. **`Type`**
- **What it is:** The universe of all types in Agda.
- **Purpose:** In Agda, types are first-class citizens, and `Type` represents the "type of types." For instance:
  - `Bool : Type` means `Bool` is a type.
  - If you define a type `ℕ : Type` for natural numbers, it also belongs to `Type`.
- **In this case:** `Bool` is defined as a type that belongs to this universe.

---

### 5. **`where`**
- **What it means:** Introduces the constructors (values) of the type.
- **Purpose:** Lists the specific ways you can construct or create values of the newly defined type.
- **In this case:** `where` introduces the two constructors, `true` and `false`, which are the only possible values of the `Bool` type.

---

### 6. **`true false`**
- **What they are:** The *constructors* of the `Bool` type.
- **Purpose:** Constructors are functions (or constants) that produce values of the type. Here:
  - `true : Bool` means `true` is a value of type `Bool`.
  - `false : Bool` means `false` is a value of type `Bool`.
- **In this case:** These two constructors define all possible values of `Bool`.

---

### 7. **`Bool` after the `:`**
- **What it means:** Specifies the type of each constructor.
- **Purpose:** Ensures that each constructor produces a value of the correct type (`Bool` in this case).
- **In this case:** Both `true` and `false` are of type `Bool`.

---

### Complete Meaning
The entire definition can be read as:
1. Define a new type called `Bool`.
2. `Bool` belongs to the universe of types (`Type`).
3. The `Bool` type has two constructors:
   - `true` (a value of type `Bool`).
   - `false` (a value of type `Bool`).

---

### Example Usage in Agda
You can use `Bool` in various ways:
```agda
-- A function that negates a Bool
not : Bool → Bool
not true = false
not false = true

-- A value of type Bool
myBool : Bool
myBool = true
```

This showcases how the `Bool` type and its constructors (`true` and `false`) can be used in programs.