### Install Mikrokosmos from Source

Source: https://github.com/mroman42/mikrokosmos/blob/master/docs/userguide.org

Manual installation steps by cloning the repository and using build tools.

```sh
git clone https://github.com/mroman42/mikrokosmos.git
cd mikrokosmos
cabal install
```

```sh
git clone https://github.com/mroman42/mikrokosmos.git
cd mikrokosmos
stack install
```

--------------------------------

### Install Mikrokosmos via Stack

Source: https://context7.com/mroman42/mikrokosmos/llms.txt

Install the Mikrokosmos interpreter using the Stack build tool. This involves cloning the repository and then running the install command.

```bash
git clone https://github.com/mroman42/mikrokosmos.git
cd mikrokosmos
stack install
```

--------------------------------

### Sample Output Styling

Source: https://github.com/mroman42/mikrokosmos/blob/master/docs/styles/readtheorg/readtheorg.org

Styling for general example output blocks.

```css
.example{
    background:#f3f6f6;
    border:1px solid #e1e4e5;
    color:#404040;
    font-size: 12px;
    line-height: 1.5;
    margin-bottom:24px;
    padding:12px;
}
```

--------------------------------

### Install Mikrokosmos via Cabal

Source: https://github.com/mroman42/mikrokosmos/blob/master/docs/userguide.org

Standard installation procedure using the Cabal package manager.

```sh
cabal update
cabal install mikrokosmos
```

--------------------------------

### Install Stack Tool

Source: https://github.com/mroman42/mikrokosmos/blob/master/CONTRIBUTING.md

Install the stack tool, a build tool for Haskell projects, before contributing to Mikrokosmos.

```bash
stack install
```

--------------------------------

### Install Mikrokosmos via Cabal

Source: https://context7.com/mroman42/mikrokosmos/llms.txt

Install the Mikrokosmos interpreter using the Cabal package manager. This includes updating the package list and installing the package, or installing from source after cloning the repository.

```bash
cabal update
cabal install mikrokosmos
```

```bash
git clone https://github.com/mroman42/mikrokosmos.git
cd mikrokosmos
cabal install
```

--------------------------------

### Typed Constructor Usage

Source: https://github.com/mroman42/mikrokosmos/blob/master/docs/tutorial.org

Examples demonstrating the use of product, union, and unit constructors.

```mikrokosmos
:types on
fst (2,3)
snd (2,3)
inl true
inr false
caseof (inl 3) (mult 2) (plus 1)
caseof (inr 3) (mult 2) (plus 1)
unit
```

--------------------------------

### Install Mikrokosmos and Jupyter Kernel

Source: https://github.com/mroman42/mikrokosmos/blob/master/docs/userguide.org

Quick installation commands for the interpreter and Jupyter kernel on GNU/Linux.

```sh
cabal install mikrokosmos
sudo pip install imikrokosmos
```

--------------------------------

### Sum and Product Examples

Source: https://github.com/mroman42/mikrokosmos/blob/master/docs/tutorial.html

Calculates the sum and product of a sample list [1, 3, 4] using the previously defined `sum` and `prod` functions.

```lambda-calculus
sum (cons 1 (cons 3 (cons 4 nil)))
```

```lambda-calculus
prod (cons 1 (cons 3 (cons 4 nil)))
```

--------------------------------

### Install Mikrokosmos Jupyter Kernel

Source: https://github.com/mroman42/mikrokosmos/blob/master/docs/userguide.org

Installs the Mikrokosmos Jupyter kernel using pip. Use the -U flag to update an existing installation.

```bash
pip install imikrokosmos
```

--------------------------------

### Install Jupyter Kernel

Source: https://context7.com/mroman42/mikrokosmos/llms.txt

Install the imikrokosmos Jupyter kernel using pip. You can install from PyPI or directly from the GitHub repository for the development version.

```bash
pip install imikrokosmos
```

```bash
pip install git+https://github.com/mroman42/jupyter-mikrokosmos.git@master
```

--------------------------------

### Define Custom Library in .mkr File

Source: https://github.com/mroman42/mikrokosmos/blob/master/docs/userguide.org

Example content for a custom library file using lambda calculus definitions.

```text
# SKI combinators
S = \x.\y.\z. x z (y z)
K = \x.\y.x
I = S K K

# Schönfinkel combinators
C = \f.\x.\y.f y x
B = \f.\g.\x.f (g x)
W = \x.\y.(y y)
```

--------------------------------

### Function Composition and Partial Application

Source: https://github.com/mroman42/mikrokosmos/blob/master/docs/tutorial.org

Examples of partial application using the constant function and defining function composition.

```mikrokosmos
# Comments can be inserted starting a line with the # character
# A constant function
discard = const id
discard 2
discard id
discard const

# Function composition
compose = \f.\g.\x.f (g x)
compose id id
```

--------------------------------

### Mikrokosmos Type Constructors and Examples

Source: https://github.com/mroman42/mikrokosmos/blob/master/docs/tutorial.html

Demonstrates the usage of Mikrokosmos's product, union, and unit type constructors, including pair creation, projection, inclusion, case analysis, and the unit element.

```Mikrokosmos
(-,-)
```

```Mikrokosmos
fst
```

```Mikrokosmos
snd
```

```Mikrokosmos
inl
```

```Mikrokosmos
inr
```

```Mikrokosmos
caseof
```

```Mikrokosmos
unit
```

```Mikrokosmos
abort
```

```Mikrokosmos
absurd
```

```Mikrokosmos
types on fst (2,3) snd (2,3) inl true inr false caseof (inl 3) (mult 2) (plus 1) caseof (inr 3) (mult 2) (plus 1) unit
```

--------------------------------

### Install Jupyter Kernel

Source: https://github.com/mroman42/mikrokosmos/blob/master/docs/userguide.html

Install the Jupyter kernel for Mikrokosmos using pip. Use the -U flag to update an existing installation.

```bash
sudo pip install imikrokosmos
```

--------------------------------

### GET /librariesEnv

Source: https://github.com/mroman42/mikrokosmos/blob/master/docs/haddock/src/Interpreter.html

Retrieves the default environment configuration combined with standard libraries.

```APIDOC
## GET /librariesEnv

### Description
Returns the default environment state after loading standard libraries.

### Method
GET

### Endpoint
/librariesEnv

### Response
#### Success Response (200)
- **env** (Environment) - The environment object containing default settings and standard libraries.
```

--------------------------------

### Boolean List Function Examples

Source: https://github.com/mroman42/mikrokosmos/blob/master/docs/tutorial.html

Tests the `all` and `any` functions with sample boolean lists. The first example checks if all elements in `(cons true (cons true nil))` are true, and the second checks if any element in `(cons false (cons true nil))` is true.

```lambda-calculus
all (cons true (cons true nil))
```

```lambda-calculus
any (cons false (cons true nil))
```

--------------------------------

### List Example: cons 1 (cons 2 (cons 3 nil))

Source: https://github.com/mroman42/mikrokosmos/blob/master/docs/tutorial.html

Demonstrates the construction of a list containing elements 1, 2, and 3 using the `cons` and `nil` constructors.

```lambda-calculus
cons 1 (cons 2 (cons 3 nil))
```

--------------------------------

### Run Mikrokosmos Interpreter

Source: https://context7.com/mroman42/mikrokosmos/llms.txt

Launch the Mikrokosmos REPL. Options include starting with standard libraries, without libraries, executing a script file, or showing the version.

```bash
mikrokosmos
```

```bash
mikrokosmos --no-libs
```

```bash
mikrokosmos --exec script.mkr
```

```bash
mikrokosmos --version
```

--------------------------------

### Example: Map with succ and mult

Source: https://github.com/mroman42/mikrokosmos/blob/master/docs/tutorial.html

Demonstrates the map function with succ (successor) and mult (multiplication) operations on a list.

```Mikrokosmos
sum (map succ (cons 1 (cons 2 (cons 3 nil))))
```

```Mikrokosmos
sum (map (mult 0) (cons 1 (cons 2 (cons 3 nil))))
```

--------------------------------

### Function Composition and Discarding

Source: https://github.com/mroman42/mikrokosmos/blob/master/docs/tutorial.html

Examples of partial application using discard and function composition.

```lambda-calculus
# Comments can be inserted starting a line with the # character
# A constant function
discard = const id
discard 2
discard id
discard const
# Function composition
compose = \f.\g.\x.f (g x)
compose id id
```

--------------------------------

### Boolean Value Selection Examples

Source: https://github.com/mroman42/mikrokosmos/blob/master/docs/tutorial.org

Demonstrates how 'true' and 'false' select arguments. 'true' returns the first argument, and 'false' returns the second. This showcases their behavior as selectors.

```mikrokosmos
true 3 4
false 3 4
true true false
false true false
```

--------------------------------

### Install Jupyter Kernel Spec

Source: https://github.com/mroman42/mikrokosmos/blob/master/docs/userguide.org

Installs the Jupyter kernelspec for Mikrokosmos. This command should be run from the mikrokosmos directory.

```bash
cd mikrokosmos
sudo jupyter kernelspec install jupyter-mikrokosmos
```

--------------------------------

### Example: Filter with eq 3

Source: https://github.com/mroman42/mikrokosmos/blob/master/docs/tutorial.html

Demonstrates the filter function to select elements equal to 3 from a list.

```Mikrokosmos
length (filter (eq 3) (cons 2 (cons 3 (cons 5 nil))))
```

--------------------------------

### Code Block Styling

Source: https://github.com/mroman42/mikrokosmos/blob/master/docs/styles/readtheorg/readtheorg.org

Styles for code blocks and example containers.

```css
.codeblock-example{
    border:1px solid #e1e4e5;
    border-bottom:none;
    padding:24px;
    padding-top:48px;
    font-weight:500;
    background:#fff;
    position:relative}

.codeblock-example:after{
    content:"Example";
    position:absolute;
    top:0px;
    left:0px;
    background:#9B59B6;
    color:#fff;
    padding:6px 12px}

.codeblock-example.prettyprint-example-only{
    border:1px solid #e1e4e5;
    margin-bottom:24px}

.codeblock,pre.src,#content .literal-block{
    border:1px solid #e1e4e5;
    padding:12px;
    overflow-x:auto;
    background:#fff;
    margin:1px 0 24px 0}

pre.src{
    /* color:#404040; */
    display:block;
    font-family:Consolas,"Andale Mono WT","Andale Mono","Lucida Console","Lucida Sans Typewriter","DejaVu Sans Mono","Bitstream Vera Sans Mono","Liberation Mono","Nimbus Mono L",Monaco,"Courier New",Courier,monospace;
    font-size:12px;
    line-height:1.5;
    margin:1px 0px 24px 0px;
    overflow:auto;
    padding:12px;
    white-space:pre;
}
```

--------------------------------

### Identity Function Examples

Source: https://github.com/mroman42/mikrokosmos/blob/master/docs/tutorial.org

Basic identity function definitions and applications.

```mikrokosmos
id 3
id 2
```

--------------------------------

### Initialize Default Interpreter Environment

Source: https://github.com/mroman42/mikrokosmos/blob/master/docs/haddock/src/Environment.html

Provides the default configuration for the interpreter's environment, starting with an empty context and specific default settings for other options.

```Haskell
[defaultEnv](Environment.html#defaultEnv) :: [Environment](Environment.html#Environment)
[defaultEnv](Environment.html#defaultEnv) \
  = [Environment](Environment.html#Environment)
  {
    context     \= [emptyContext](Environment.html#emptyContext),
    loadedFiles \= \[],
    verbose     \= False,
    color       \= True,
    skioutput   \= False,
    types       \= False,
    topo        \= False
  }
```

--------------------------------

### Example: Tree traversal with triplesum

Source: https://github.com/mroman42/mikrokosmos/blob/master/docs/tutorial.html

Applies a function (triplesum) to a binary tree. The function combines the label with results from subtrees.

```Mikrokosmos
mytree = node 4 (node 2 nil nil) (node 3 nil nil)
```

```Mikrokosmos
triplesum = \a.\b.\c.plus (plus a b) c
```

```Mikrokosmos
mytree triplesum 0
```

--------------------------------

### readFileDependencies

Source: https://github.com/mroman42/mikrokosmos/blob/master/docs/haddock/src/Main.html

Reads the dependencies from a single file. It parses the file content to find lines starting with '#INCLUDE ' and returns a list of module names.

```APIDOC
## readFileDependencies

### Description
Reads the dependencies from a single file. It parses the file content to find lines starting with '#INCLUDE ' and returns a list of module names.

### Method
N/A (Function Signature)

### Endpoint
N/A

### Parameters
#### Path Parameters
N/A

#### Query Parameters
N/A

#### Request Body
N/A

### Request Example
N/A

### Response
#### Success Response (200)
- **[Modulename]** (List[String]) - A list of module names found as dependencies.

#### Response Example
N/A
```

--------------------------------

### Lambda Calculus Function Application Example

Source: https://github.com/mroman42/mikrokosmos/blob/master/docs/tutorial.html

Demonstrates a simple function application and beta-reduction in lambda calculus. The function `(λx. 2 * x)` is applied to the argument `3`.

```lambda-calculus
(λx. 2 * x) 3

→ 2 * 3

→ 6.
```

--------------------------------

### Define SKI and Schönfinkel Combinators

Source: https://github.com/mroman42/mikrokosmos/blob/master/docs/userguide.html

Example of a Mikrokosmos library file defining SKI and Schönfinkel combinators using lambda calculus notation. The Y combinator is also defined.

```mkr
# SKI combinators
S = \x.\y.\z. x z (y z)
K = \x.\y.x
I = S K K

# Schönfinkel combinators
C = \f.\x.\y.f y x
B = \f.\g.\x.f (g x)
W = \x.\y.(y y)

# Y combinator
Y := \f.(\x.f (x x))(\x.f (x x))
```

--------------------------------

### Example: Fixpoint with const id

Source: https://github.com/mroman42/mikrokosmos/blob/master/docs/tutorial.html

Demonstrates the fix combinator with a constant identity function. Note: Evaluating 'fix' alone leads to an infinite loop.

```Mikrokosmos
fix (const id)
```

--------------------------------

### Main Entry Point for Lambda Interpreter

Source: https://github.com/mroman42/mikrokosmos/blob/master/docs/haddock/src/Main.html

Sets up the initial environment based on flags and handles command-line arguments for running the interpreter interactively or executing a file.

```haskell
main :: IO ()
main = 
  runCommand $ \opts args -> do
  let initialEnv = if flagLibs opts then defaultEnv else librariesEnv
  if flagVersion opts
  then putStrLn versionText
  else case args of
             [] -> 
               runInputT 
                 defaultSettings 
                 (outputStrLn initialText >> interpreterLoop initialEnv)
             [filename] -> executeFile filename
             _ -> putStrLn "Wrong number of arguments"
```

--------------------------------

### Environment and Loading Functions

Source: https://github.com/mroman42/mikrokosmos/blob/master/docs/haddock/doc-index-L.html

Documentation for librariesEnv, Load, and loadFile.

```APIDOC
## Environment and Loading Functions

### Description
Documentation for environment related types and functions like librariesEnv, Load, and loadFile.

### Endpoint
/mroman42/mikrokosmos/Interpreter.html#v:librariesEnv
/mroman42/mikrokosmos/Interpreter.html#v:Load
/mroman42/mikrokosmos/Main.html#v:loadFile
```

--------------------------------

### Install Development Version of Jupyter Kernel

Source: https://github.com/mroman42/mikrokosmos/blob/master/docs/userguide.org

Installs a development version of the Jupyter kernel from its GitHub repository's master branch.

```bash
pip install git+https://github.com/mroman42/jupyter-mikrokosmos.git@master
```

--------------------------------

### Mikrokosmos Example: Identity Function

Source: https://github.com/mroman42/mikrokosmos/blob/master/docs/tutorial.html

An example using the Mikrokosmos interpreter to define and apply the identity function (`id = \x.x`). Mikrokosmos accepts `\` as a lambda symbol.

```mikrokosmos
# Our first example
id = \x.x
id id

# More examples on the identity function
id 3
id 2
```

--------------------------------

### Exercise 1.2 Template

Source: https://github.com/mroman42/mikrokosmos/blob/master/docs/tutorial.org

Template for implementing application and flip functions.

```mikrokosmos
# -- Your solutions go here
# app = 
```

--------------------------------

### Index - I

Source: https://github.com/mroman42/mikrokosmos/blob/master/docs/haddock/doc-index-I.html

This section indexes various Haskell functions and types starting with the letter 'I'.

```APIDOC
## Index - I

### Description
This section indexes various Haskell functions and types starting with the letter 'I'.

### Functions and Types:

- **Ski**: [Ski.html#v:I]
- **incrementindices**: [Stlc.Types.html#v:incrementindices]
- **initialText**: [Format.html#v:initialText]
- **Inl**: [Lambda.html#v:Inl]
- **Inr**: [Lambda.html#v:Inr]
- **insert**: [MultiBimap.html#v:insert]
- **Interpret**: [Interpreter.html#v:Interpret]
- **InterpreterAction**: [Interpreter.html#t:InterpreterAction]
- **interpreteractionParser**: [Interpreter.html#v:interpreteractionParser]
- **interpreterLoop**: [Main.html#v:interpreterLoop]
- **isOpenExp**: [Lambda.html#v:isOpenExp]

### Generated By
Produced by [Haddock](http://www.haskell.org/haddock/) version 2.17.3
```

--------------------------------

### Exercise: Implement All and Any

Source: https://github.com/mroman42/mikrokosmos/blob/master/docs/tutorial.org

Template for implementing boolean list functions using fold.

```mikrokosmos
# -- Your solution goes here. Uncomment the following lines
# all = 
# any =

all (cons true  (cons true nil))
any (cons false (cons true nil))
```

--------------------------------

### Loading Libraries

Source: https://context7.com/mroman42/mikrokosmos/llms.txt

Load custom libraries into the environment.

```haskell
# Library search paths:
# - ./
# - ./lib/
# - ~/.mikrokosmos/
# - ~/

# Load a library
:load mylib

# Libraries are loaded with :load <name> (without .mkr extension)
```

--------------------------------

### Evaluate Lambda Expressions in Mikrokosmos

Source: https://github.com/mroman42/mikrokosmos/blob/master/docs/index.org

Demonstrates basic lambda syntax, library usage, type system toggling, and deduction tree generation within the Mikrokosmos console.

```text
# Lambda expressions are written with \ or λ, as in
(λx.x)
(\x.\y.x)(\x.x)

# Libraries included
plus 2 3
sum (cons 1 (cons 2 (cons 3 nil)))

# Change between untyped and simply-typed λ-calculus
:types on
swap = \m.(snd m, fst m)
swap

# Gentzen-style deduction trees
@@ \a.(snd a,fst a)
```

--------------------------------

### Parse Diagram Request

Source: https://github.com/mroman42/mikrokosmos/blob/master/docs/haddock/src/Interpreter.html

Parses a command to generate a diagram from a lambda expression. Starts with '@ '.

```Haskell
diagramParser :: Parser [Action]
diagramParser = Diagram <$> (string "@ " >> lambdaexp)
```

--------------------------------

### Define Libraries Environment

Source: https://github.com/mroman42/mikrokosmos/blob/master/docs/haddock/src/Interpreter.html

Initializes the environment with standard libraries.

```haskell
librariesEnv :: [Environment]
librariesEnv = snd $ executeWithEnv defaultEnv stdlibraries
```

--------------------------------

### Example: Calculate factorial

Source: https://github.com/mroman42/mikrokosmos/blob/master/docs/tutorial.html

Calculates the factorial of a number using the previously defined 'fact' function.

```Mikrokosmos
fact 3
```

```Mikrokosmos
fact 4
```

--------------------------------

### Placeholder for solution

Source: https://github.com/mroman42/mikrokosmos/blob/master/docs/tutorial.org

A template block used for user exercises.

```mikrokosmos
# -- Your solution goes here
```

--------------------------------

### Parse Simplified Diagram Request

Source: https://github.com/mroman42/mikrokosmos/blob/master/docs/haddock/src/Interpreter.html

Parses a command to generate a simplified diagram from a lambda expression. Starts with '@@ '.

```Haskell
simpdiagramParser :: Parser [Action]
simpdiagramParser = SimpDiagram <$> (string "@@ " >> lambdaexp)
```

--------------------------------

### Exercise 1.2 Lambda Terms

Source: https://github.com/mroman42/mikrokosmos/blob/master/docs/tutorial.html

Placeholder for defining application and flip functions.

```lambda-calculus
# -- Your solutions go here
# app =
# flip =
app not true
flip const 4 3
```

--------------------------------

### Enable and use typed lambda calculus

Source: https://github.com/mroman42/mikrokosmos/blob/master/docs/tutorial.html

Activates type checking and demonstrates function application with types.

```Mikrokosmos
:types on
# Some examples
id
K
fix

# Function application
plus
plus 3
plus 3 2
```

--------------------------------

### Equality and Less Than or Equal To Predicates

Source: https://github.com/mroman42/mikrokosmos/blob/master/docs/tutorial.org

Builds 'eq' (equality) and 'leq' (less than or equal to) predicates using the 'iszero' function and 'minus'.

```mikrokosmos
leq = 
.(iszero (minus m n))
eq  = 
.(and (leq m n) (leq n m))

leq 2 3
leq 4 1
eq  5 5
```

--------------------------------

### Define Initial Interpreter Text

Source: https://github.com/mroman42/mikrokosmos/blob/master/docs/haddock/src/Format.html

The welcome message and version information displayed when the Mikrokosmos interpreter starts. Uses 'unlines' for formatting.

```Haskell
initialText :: String
initialText = unlines [
  formatIntro ++ "Welcome to the Mikrokosmos Lambda Interpreter!" ++ end,
  formatFormula ++ "Version " ++ version ++ ". GNU General Public License Version 3." ++ end
  ]
```

--------------------------------

### Example: Calculate Fibonacci numbers

Source: https://github.com/mroman42/mikrokosmos/blob/master/docs/tutorial.html

Calculates Fibonacci numbers for small inputs using the 'fib' function. High inputs can lead to non-termination.

```Mikrokosmos
fib 0
```

```Mikrokosmos
fib 1
```

```Mikrokosmos
fib 2
```

```Mikrokosmos
fib 3
```

```Mikrokosmos
fib 4
```

--------------------------------

### showProofTree

Source: https://github.com/mroman42/mikrokosmos/blob/master/docs/haddock/Stlc-Gentzen.html

Draws a complete derivation tree from a ProofTree structure.

```APIDOC
## showProofTree

### Description
Draws a complete derivation tree.

### Type Signature
showProofTree :: ProofTree String String -> String

### Parameters
#### Path Parameters
None

#### Query Parameters
None

#### Request Body
None

### Request Example
None

### Response
#### Success Response (200)
- **String** - A string representation of the derivation tree.

#### Response Example
None
```

--------------------------------

### Exercise: Implement List Transformations

Source: https://github.com/mroman42/mikrokosmos/blob/master/docs/tutorial.org

Template for implementing list doubling and boolean negation functions.

```mikrokosmos
# -- Your solution goes here
# doublelist =
# negate =
```

--------------------------------

### Read File Dependencies

Source: https://github.com/mroman42/mikrokosmos/blob/master/docs/haddock/src/Main.html

Reads a file to extract module dependencies. It handles potential IO errors and filters for lines starting with '#INCLUDE '.

```Haskell
readFileDependencies :: [Filename](Environment.html#Filename) -> IO [[Modulename](Environment.html#Modulename)]
[readFileDependencies](Main.html#readFileDependencies) [filename](#local-6989586621679047828) = do
  [input](#local-6989586621679047829) <- try $ readFile [filename](#local-6989586621679047828) :: IO (Either IOException String)
  case [input](#local-6989586621679047829) of
    Left _ -> return []
    Right [inputs](#local-6989586621679047830) -> return $
      map (drop 9) (filter (isPrefixOf "#INCLUDE ") (filter (/="") $ lines [inputs](#local-6989586621679047830)))
```

--------------------------------

### Custom Library Creation

Source: https://context7.com/mroman42/mikrokosmos/llms.txt

Define custom combinators and modules in .mkr files.

```haskell
# File: mylib.mkr
# Custom SKI combinators
S = \x.\y.\z.x z (y z)
K = \x.\y.x
I = S K K

# Schönfinkel combinators
C = \f.\x.\y.f y x
B = \f.\g.\x.f (g x)
W = \x.\y.(y y)

# Y combinator (delayed binding)
Y := \f.(\x.f (x x))(\x.f (x x))

# Module dependency declaration
#INCLUDE othermodule
```

--------------------------------

### Basic Lambda Calculus Expressions in Mikrokosmos

Source: https://github.com/mroman42/mikrokosmos/blob/master/docs/tutorial.org

Demonstrates fundamental lambda calculus expressions like identity (id), constant (K), and fixed-point combinator (fix). Also shows function application with 'plus'.

```mikrokosmos
id
```

```mikrokosmos
K
```

```mikrokosmos
fix
```

```mikrokosmos
plus
```

```mikrokosmos
plus 3
```

```mikrokosmos
plus 3 2
```

--------------------------------

### Constant Function and Application

Source: https://github.com/mroman42/mikrokosmos/blob/master/docs/tutorial.html

Demonstrates the constant function and its application in lambda calculus.

```lambda-calculus
const = \x.\y.x
const 3 4
const id id
const id const
```

--------------------------------

### POST /executeWithEnv

Source: https://github.com/mroman42/mikrokosmos/blob/master/docs/haddock/src/Interpreter.html

Executes a block of code within a provided environment and returns the output and the updated environment.

```APIDOC
## POST /executeWithEnv

### Description
Executes a block of code in a given environment. It parses the input code, performs the actions, and returns the resulting output string and the modified environment.

### Method
POST

### Endpoint
/executeWithEnv

### Parameters
#### Request Body
- **initEnv** (Environment) - Required - The initial environment state.
- **code** (String) - Required - The block of code to be executed.

### Response
#### Success Response (200)
- **output** (String) - The result of the execution.
- **env** (Environment) - The updated environment state.

### Response Example
{
  "output": "result string",
  "env": "updated_environment_object"
}
```

--------------------------------

### Load and Execute File Actions

Source: https://github.com/mroman42/mikrokosmos/blob/master/docs/haddock/src/Main.html

Loads a file, parses its content into actions, and executes them. Returns an error message if the file cannot be loaded.

```Haskell
loadFile :: [Filename](Environment.html#Filename) -> IO (Maybe [[Action](Interpreter.html#Action)])
[loadFile](Main.html#loadFile) [filename](#local-6989586621679047473) = do
  putStrLn $ [formatLoading](Format.html#formatLoading) ++ "Loading " ++ [filename](#local-6989586621679047473) ++ "..." ++ [end](Format.html#end)
  [input](local-6989586621679047818) <- try $ readFile [filename](#local-6989586621679047473) :: IO (Either IOException String)
  case [input](local-6989586621679047818) of
    Left _ -> return Nothing
    Right [inputs](local-6989586621679047819) -> do
      let [parsing](local-6989586621679047820) = map (parse [actionParser](Interpreter.html#actionParser) "" . [preformat](Interpreter.html#preformat)) . filter (/="") . lines $ [inputs](local-6989586621679047819)
      let [actions](local-6989586621679047821) = map (\ [x](local-6989586621679047822) -> case [x](local-6989586621679047822) of
                                 Left _  -> Nothing
                                 Right [a](local-6989586621679047823) -> Just [a](local-6989586621679047823)) [parsing](local-6989586621679047820)
      return $ sequence [actions](local-6989586621679047821)

[executeFile](Main.html#executeFile) :: [Filename](Environment.html#Filename) -> IO ()
[executeFile](Main.html#executeFile) [filename](local-6989586621679047824) = do
  [maybeloadfile](local-6989586621679047825) <- [loadFile](Main.html#loadFile) [filename](local-6989586621679047824)
  case [maybeloadfile](local-6989586621679047825) of
    Nothing -> putStrLn "Error loading file"
    Just [actions](local-6989586621679047826) ->
      case runState ([multipleAct](Interpreter.html#multipleAct) [actions](local-6989586621679047826)) [defaultEnv](Environment.html#defaultEnv) of
        ([outputs](local-6989586621679047827), _) -> mapM_ putStr [outputs](local-6989586621679047827)
```

--------------------------------

### Define Version Complete Text

Source: https://github.com/mroman42/mikrokosmos/blob/master/docs/haddock/src/Format.html

A string combining the product name and version number.

```Haskell
versionText :: String
versionText = "Mikrokosmos, version " ++ version
```

--------------------------------

### readAllModuleDepsRecursively

Source: https://github.com/mroman42/mikrokosmos/blob/master/docs/haddock/src/Main.html

Reads module dependencies recursively. It starts with a list of module names and continues to find dependencies until no new modules are discovered. Returns an error if any dependency cannot be found.

```APIDOC
## readAllModuleDepsRecursively

### Description
Reads module dependencies recursively. It starts with a list of module names and continues to find dependencies until no new modules are discovered. Returns an error if any dependency cannot be found.

### Method
N/A (Function Signature)

### Endpoint
N/A

### Parameters
#### Path Parameters
N/A

#### Query Parameters
N/A

#### Request Body
N/A

### Request Example
N/A

### Response
#### Success Response (200)
- **[Modulename]** (Maybe[List[String]]) - A list of all recursively found module names, or Nothing if an error occurred.

#### Response Example
N/A
```

--------------------------------

### Execute λ-calculus expression in Mikrokosmos

Source: https://github.com/mroman42/mikrokosmos/blob/master/docs/tutorial.org

Demonstrates the basic syntax for function application in the Mikrokosmos interpreter.

```text
(λx.mult 2 x) 3
```

--------------------------------

### POST :load

Source: https://github.com/mroman42/mikrokosmos/blob/master/docs/haddock/src/Interpreter.html

Parses the command to load a file into the interpreter.

```APIDOC
## POST :load

### Description
Parses the load-file command followed by a file path.

### Method
POST

### Endpoint
:load [filepath]

### Parameters
#### Path Parameters
- **filepath** (string) - Required - The path to the file to be loaded.
```

--------------------------------

### Define and use a tree structure

Source: https://github.com/mroman42/mikrokosmos/blob/master/docs/tutorial.org

Demonstrates basic node construction and a triple summation function applied to a tree.

```mikrokosmos
mytree    = node 4 (node 2 nil nil) (node 3 nil nil)
triplesum = \a.\b.\c.plus (plus a b) c
mytree triplesum 0
```

--------------------------------

### Swap Function Simplification in Mikrokosmos

Source: https://github.com/mroman42/mikrokosmos/blob/master/docs/tutorial.html

Compares the derivation trees of the `swap` function in Mikrokosmos before and after simplification using `@` and `@@` commands, illustrating the Curry-Howard isomorphism between term evaluation and proof simplification.

```Mikrokosmos
@ \m.(snd m,fst m)
```

```Mikrokosmos
@@ \m.(snd m,fst m)
```

--------------------------------

### Lambda Abstraction and Application

Source: https://github.com/mroman42/mikrokosmos/blob/master/docs/haddock/doc-index-L.html

Documentation for LambdaAbstraction and LambdaApplication, referencing NamedLambda.

```APIDOC
## LambdaAbstraction and LambdaApplication

### Description
Documentation for LambdaAbstraction and LambdaApplication, which are related to NamedLambda.

### Endpoint
/mroman42/mikrokosmos/NamedLambda.html#v:LambdaAbstraction
/mroman42/mikrokosmos/NamedLambda.html#v:LambdaApplication
```

--------------------------------

### File Execution and Loading

Source: https://github.com/mroman42/mikrokosmos/blob/master/docs/haddock/Main.html

Endpoints for loading and executing .mkr files and managing module dependencies.

```APIDOC
## loadFile

### Description
Loads the given filename and returns the complete list of actions. Returns Nothing if there is an error reading or parsing the file.

### Parameters
- **Filename** (String) - Required - The path to the .mkr file to load.

## executeFile

### Description
Executes the commands inside a file. A .mkr file can contain a sequence of expressions and variable bindings, and it is interpreted sequentially.

### Parameters
- **Filename** (String) - Required - The path to the .mkr file to execute.

## readFileDependencies

### Description
Reads module dependencies from a given file.

### Parameters
- **Filename** (String) - Required - The path to the file to analyze for dependencies.
```

--------------------------------

### Format and Output Actions

Source: https://github.com/mroman42/mikrokosmos/blob/master/docs/haddock/src/Main.html

Formats and prints a list of output strings to the console. It applies color formatting based on the environment's color setting.

```Haskell
[outputActions](Main.html#outputActions) :: [Environment](Environment.html#Environment) -> [String] -> InputT IO ()
[outputActions](Main.html#outputActions) [environment](local-6989586621679047468) [output](local-6989586621679047469) = do
    outputStr (if [getColor](Environment.html#getColor) [environment](local-6989586621679047468) then [formatFormula](Format.html#formatFormula) else "")
    mapM_ (outputStr . [format](local-6989586621679047470)) [output](local-6989586621679047469)
    outputStr [end](Format.html#end)
  where
    [format](local-6989586621679047470) = [formatColor](local-6989586621679047471)
    [formatColor](local-6989586621679047471) [s](local-6989586621679047472)
      | [getColor](Environment.html#getColor) [environment](local-6989586621679047468) = [s](local-6989586621679047472)
      | otherwise            = unlines $ map [decolor](Format.html#decolor) $ lines [s](local-6989586621679047472)
```

--------------------------------

### Run Tests with Stack

Source: https://github.com/mroman42/mikrokosmos/blob/master/CONTRIBUTING.md

Ensure all project tests pass using the stack test command before committing changes or submitting a pull request.

```bash
stack test
```

--------------------------------

### Implement Show Instance for Ski

Source: https://github.com/mroman42/mikrokosmos/blob/master/docs/haddock/src/Ski.html

Custom string representation for SKI combinator expressions.

```haskell
instance Show Ski where
  show = showski

-- | Shows a SKI expression
showski :: Ski -> String
showski S = "S"
showski K = "K"
showski I = "I"
showski (Cte _) = "?"
showski (Comb x S) = showski x ++ showski S
showski (Comb x K) = showski x ++ showski K
showski (Comb x I) = showski x ++ showski I
showski (Comb x (Cte c)) = showski x ++ showski (Cte c)
showski (Comb x (Comb u v)) = showski x ++ "(" ++ showski (Comb u v) ++ ")"
showski (Comb x a) = showski x ++ showski a
showski Spair = "[PAIR]"
showski Spi1 = "[FST]"
showski Spi2 = "[SND]"
showski Sinl = "[INL]"
showski Sinr = "[INR]"
showski Scase = "[CASEOF]"
showski Sunit = "[UNIT]"
showski Sabort = "[ABORT]"
showski Sabsurd = "[ABSURD]"
```

--------------------------------

### Show Derivation Tree in Mikrokosmos

Source: https://github.com/mroman42/mikrokosmos/blob/master/docs/tutorial.org

Use '@@' to display the derivation tree of a proof in Mikrokosmos. This is useful for understanding the structure of a proof.

```mikrokosmos
:types on
# Our proof is of type (A + B) → B + A
\m.caseof m inr inl

# And we can show a derivation tree of it as
@@ \m.caseof m inr inl

# A simpler example is the identity
@@ \x.x
```

--------------------------------

### Exercise 1.1 Expressions

Source: https://github.com/mroman42/mikrokosmos/blob/master/docs/tutorial.html

Placeholder for evaluating composition expressions.

```lambda-calculus
# -- Your solution goes here
# Feel free to play with the interpreter!
```

--------------------------------

### Identity Proof with Derivation Tree in Mikrokosmos

Source: https://github.com/mroman42/mikrokosmos/blob/master/docs/tutorial.html

Provides a simple identity proof (x → x) in Mikrokosmos and displays its derivation tree using the `@@` command, illustrating the interpreter's proof visualization capabilities.

```Mikrokosmos
# A simpler example is the identity @@ \x.x
```

--------------------------------

### Proof of Disjunction Commutativity with Derivation Tree in Mikrokosmos

Source: https://github.com/mroman42/mikrokosmos/blob/master/docs/tutorial.html

Proves A ∨ B → B ∨ A in Mikrokosmos and shows its derivation tree using the `@@` command. This demonstrates how the interpreter can visualize proof structures.

```Mikrokosmos
# Our proof is of type (A + B) → B + A \m.caseof m inr inl # And we can show a derivation tree of it as @@ \m.caseof m inr inl
```

--------------------------------

### Sum and Product on Lists using Fold

Source: https://github.com/mroman42/mikrokosmos/blob/master/docs/tutorial.html

Implements `sum` and `prod` functions using the generic `fold` function. `sum` uses `plus` and `0`, while `prod` uses `mult` and `1` as parameters to `fold`.

```lambda-calculus
sum = fold plus 0
```

```lambda-calculus
prod = fold mult 1
```

--------------------------------

### Create Mikrokosmos Code Pad

Source: https://github.com/mroman42/mikrokosmos/blob/master/docs/userguide.org

Use a div with the class 'mikrojs-console' and a script tag with type 'text/mikrokosmos' to render an interactive code pad.

```html
<div class="mikrojs-console">
<script type="text/mikrokosmos">
:ski on
S = λa.λb.λc.(a c) (b c)
K = λa.λb.a
I = λa.a

# Exercise. Write the natural numbers in terms of lambda 
# expressions using Church encoding. The interpreter will
# translate them into SKI combinators. Describe the pattern the
# natural numbers follow in terms of SKI combinators.

# Your code goes here.</script>
</div>
```

--------------------------------

### Load File

Source: https://github.com/mroman42/mikrokosmos/blob/master/docs/haddock/src/Main.html

Loads a specified file and returns a list of actions. Returns Nothing if there is an error reading or parsing the file.

```APIDOC
## LOAD FILE

### Description
Loads the given filename and returns the complete list of actions. Returns Nothing if there is an error reading or parsing the file.

### Method
GET

### Endpoint
/load/file

### Parameters
#### Query Parameters
- **filename** (string) - Required - The name of the file to load.

### Request Body
This endpoint does not require a request body.

### Response
#### Success Response (200)
- **actions** (array) - A list of actions parsed from the file.

#### Response Example
{
  "actions": [
    {
      "type": "Expression",
      "value": "1 + 1"
    }
  ]
}
```