initial

2025-12-14 21:07:46 +00:00
commit 5db24213bd
281 changed files with 18445 additions and 0 deletions
--- a/20250120113936-afp_lab_1.org
+++ b/20250120113936-afp_lab_1.org
@@ -0,0 +1,115 @@
+: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.