### Compile with Installed Package

Source: https://github.com/idris-lang/idris2/blob/main/docs/source/reference/packages.md

Example of compiling 'Main.idr' while making the 'test' package accessible using the '-p' or '--package' flag.

```bash
idris -p test Main.idr
```

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

### Example Program Run

Source: https://github.com/idris-lang/idris2/blob/main/docs/source/tutorial/interp.md

Demonstrates an example execution of the Idris interpreter program, showing user interaction and the output of the factorial calculation.

```default
$ idris2 interp.idr
     ____    __     _         ___ 
    /  _/___/ /____(_)____   |__ \
    / // __  / ___/ / ___/   __/ /     Version 0.8.0
  _/ // /_/ / /  / (__  )   / __/      https://www.idris-lang.org
 /___/\__,_/_/  /_/____/   /____/      Type :? for help

Welcome to Idris 2.  Enjoy yourself!
Main> :exec main
Enter a number: 6
720
```

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

### Install Idris 2 library documentation

Source: https://github.com/idris-lang/idris2/blob/main/INSTALL.md

After installing Idris 2, run this command to install the library documentation. The index file will be located in the `docs` subdirectory of the Idris 2 library directory.

```sh
make install-libdocs
```

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

### Install an Idris Package

Source: https://github.com/idris-lang/idris2/blob/main/docs/source/tutorial/packages.md

Use the --install command with the package file name to install the package, making it available for other projects.

```default
idris2 --install maths.ipkg
```

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

### Install a Package

Source: https://github.com/idris-lang/idris2/blob/main/docs/source/reference/packages.md

Command to install the 'test.ipkg' package to the global Idris library directory, making its modules accessible to other projects.

```bash
idris2 --install test.ipkg
```

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

### Install Idris 2 Docs Dependencies with Uv

Source: https://github.com/idris-lang/idris2/blob/main/docs/README.md

Installs necessary dependencies for building Idris 2 documentation using uv within a virtual environment. Ensure uv is installed.

```sh
uv sync
uv venv
source .venv/bin/activate
```

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

### Build and install Idris 2 from source with an existing compiler

Source: https://github.com/idris-lang/idris2/blob/main/INSTALL.md

If you have a recent released version of Idris 2 installed, use these commands to build and install the latest version from source.

```sh
make all
make install
```

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

### Set Idris 2 Installation Prefix

Source: https://github.com/idris-lang/idris2/blob/main/docs/source/tutorial/starting.md

Configure the installation directory for Idris 2. By default, it installs to ${HOME}/.idris2. This example shows how to set it to /usr/local.

```makefile
IDRIS2_PREFIX ?= /usr/local
```

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

### Self-hosting Idris 2

Source: https://github.com/idris-lang/idris2/blob/main/INSTALL.md

Rebuild and install Idris 2 from the newly compiled version to verify the installation. Ensure 'idris2' is in your PATH.

```makefile
make clean
make all && make install
```

```makefile
make all IDRIS2_BOOT='idris2 --codegen racket' && make install
```

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

### Install Idris 2 after bootstrapping

Source: https://github.com/idris-lang/idris2/blob/main/INSTALL.md

After successfully bootstrapping Idris 2 from source, use this command to install it to the target directory specified in `config.mk`.

```sh
make install
```

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

### Re-bootstrap and install Idris libraries

Source: https://github.com/idris-lang/idris2/wiki/FAQ:-Working-on-Idris

If libraries are compiled but not installed, run `make install`. If issues persist, re-bootstrap with a specific SCHEME and then run `make install`.

```bash
make install
```

```bash
make bootstrap SCHEME=chez
make install
```

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

### Install Build Dependencies with pacman

Source: https://github.com/idris-lang/idris2/blob/main/docs/source/tutorial/windows.md

Installs the 'make' utility and the GCC compiler for Windows 64-bit within the MSYS2 environment. Ensure MSYS2 is updated before running.

```bash
$ pacman -S make mingw-w64-x86_64-gcc
```

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

### Install Idris 2 with Nix Flakes

Source: https://github.com/idris-lang/idris2/blob/main/INSTALL.md

Install Idris 2 directly from its GitHub repository using Nix Flakes. This method ensures you get the latest version from the repository.

```sh
nix profile install github:idris-lang/Idris2
```

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

### StoreI Interface Implementation

Source: https://github.com/idris-lang/idris2/blob/main/docs/source/app/linear.md

An example implementation of the `StoreI` interface with hardcoded credentials and data. It uses `pure1` to lift results into `App1`.

```idris
Has [Console] e => StoreI e where
  connect
      = do app $ putStrLn "Connect"
           pure1 (MkStore "xyzzy")

  login (MkStore str) pwd
      = if pwd == "Mornington Crescent"
           then pure1 (True # MkStore str)
           else pure1 (False # MkStore str)
  logout (MkStore str) = pure1 (MkStore str)
  readSecret (MkStore str) = pure1 (str # MkStore str)

  disconnect (MkStore _)
      = putStrLn "Disconnect"
```

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

### Example Program Using App1 and App

Source: https://github.com/idris-lang/idris2/blob/main/docs/source/app/linear.md

Demonstrates using `app1` to enter a linear context and `app` for non-linear operations like `putStr` within that context.

```idris
storeProg : Has [Console, StoreI] e => App e ()
storeProg = app1 $ do
     store <- connect
     app $ putStr "Password: "
     ?what_next
```

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

### Example of Adding a Student

Source: https://github.com/idris-lang/idris2/blob/main/docs/source/tutorial/typesfuns.md

Demonstrates the usage of the 'addStudent' function by adding 'fred' to an empty 'CS' class.

```default
*Record> addStudent fred (ClassInfo [] "CS")
ClassInfo [MkPerson "Fred" "Joe" "Bloggs" 30] "CS" : Class
```

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

### Install Idris 2 with Homebrew

Source: https://github.com/idris-lang/idris2/blob/main/INSTALL.md

Use this command to install Idris 2 if you are using macOS or Linux and have Homebrew installed.

```sh
brew install idris2
```

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

### Install Idris 2 using Yay

Source: https://github.com/idris-lang/idris2/blob/main/docs/source/tutorial/starting.md

Install Idris 2 and its dependencies on Arch Linux or Arch-based distributions using the Yay AUR helper.

```bash
yay -S idris2
```

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

### Do Notation Example: Sequential Binding

Source: https://github.com/idris-lang/idris2/blob/main/docs/source/typedd/typedd.md

Shows how a do block with sequential binding (<-) is desugared into chained >>= operations.

```idris
do
  x <- foo
  y <- bar
  baz x y
```

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

### Example Interpreter Usage (Success)

Source: https://github.com/idris-lang/idris2/blob/main/docs/source/tutorial/interfaces.md

Demonstrates a successful evaluation of an arithmetic expression using the runEval function.

```default
InterpE> runEval [("x", 10), ("y",84)] (Add (Var "x") (Var "y"))
Just 94
```

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

### List Desugaring Example

Source: https://github.com/idris-lang/idris2/wiki/What-Contributions-are-Needed

Illustrates how list syntax like `[ x1 , x2, x3 ]` is desugared into a sequence of cons operations and a final Nil constructor. This example highlights how source location information might be handled.

```idris
[ x1 , x2, x3 ]
```

```idris
x1 :: x2 :: x3 :: Nil
```

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

### Basic App Program Example

Source: https://github.com/idris-lang/idris2/blob/main/docs/source/app/introapp.md

A simple App program that performs console output. Requires the Console interface.

```idris
hello : Console es => App es ()
hello = putStrLn "Hello, App world!"
```

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

### Install Idris 2 using DNF

Source: https://github.com/idris-lang/idris2/blob/main/docs/source/tutorial/starting.md

Install Idris 2 and its dependencies on Fedora or EPEL-enabled systems using the DNF package manager.

```bash
sudo dnf install idris2
```

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

### Installing Idris 2 API

Source: https://github.com/idris-lang/idris2/blob/main/INSTALL.md

Install the Idris 2 API, necessary for developing external support tools like code generators. This step requires the self-hosting step to be completed.

```makefile
make install-api
```

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

### Tuple Examples in Idris

Source: https://github.com/idris-lang/idris2/blob/main/docs/source/tutorial/typesfuns.md

Demonstrates the creation and usage of tuples in Idris, including nested tuples and accessing elements.

```idris
fred : (String, Int)
fred = ("Fred", 42)

jim : (String, Int, String)
jim = ("Jim", 25, "Cambridge")
```

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

### Correct Door Protocol Usage Example

Source: https://github.com/idris-lang/idris2/blob/main/docs/source/tutorial/multiplicities.md

An example of a correctly implemented door protocol. It uses `newDoor` to create a door, then opens and closes it, and finally deletes it, adhering to the linear usage requirements.

```idris
doorProg : IO ()
doorProg
    = newDoor $ \d =>
          let d' = openDoor d
              d'' = closeDoor d' in
              deleteDoor d''
```

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

### Proof Search Example with vzipWith

Source: https://github.com/idris-lang/idris2/blob/main/docs/source/tutorial/interactive.md

Demonstrates using `:ps` to find a value for a hole in a function definition. This works by analyzing the type signature and available constructors.

```idris
vzipWith : (a -> b -> c) ->
           Vect n a -> Vect n b -> Vect n c
vzipWith f [] [] = ?vzipWith_rhs_1
vzipWith f (x :: xs) (y :: ys) = ?vzipWith_rhs_2
```

```text
:ps 96 vzipWith_rhs_1
[]
```

```text
:ps 97 vzipWith_rhs_2
f x y :: vzipWith f xs ys
```

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

### Bash Auto-completion Setup

Source: https://github.com/idris-lang/idris2/blob/main/INSTALL.md

Configure tab auto-completion for Idris 2 in Bash shells. Add the command to your .bashrc for persistent setup.

```bash
eval "$(idris2 --bash-completion-script idris2)"
```

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

### Literate Programming Example in Idris

Source: https://github.com/idris-lang/idris2/blob/main/docs/source/tutorial/miscellany.md

Demonstrates literate programming in Idris, where code lines are prefixed with '>' and comments are otherwise.

```default
> module literate

This is a comment. The main program is below

> main : IO ()
> main = putStrLn "Hello literate world!\n"
```

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

### Example of Monadic Addition with Just Values

Source: https://github.com/idris-lang/idris2/blob/main/docs/source/tutorial/interfaces.md

Demonstrates the `m_add` function with two `Just` values, showing a successful addition.

```default
Main> m_add (Just 82) (Just 22)
Just 104
```

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

### Interactive Type Matching Examples

Source: https://github.com/idris-lang/idris2/blob/main/docs/source/tutorial/multiplicities.md

Illustrates the behavior of the `showType` function with different types in an interactive session.

```default
Main> showType Int
"Int"
Main> showType (List Int)
"List of Int"
Main> showType (List Bool)
"List of something else"
```

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

### Idris 2 Hello World Program

Source: https://github.com/idris-lang/idris2/blob/main/docs/source/tutorial/starting.md

A basic 'Hello, World!' program in Idris 2. This file can be used to verify a successful installation.

```idris
module Main

main : IO ()
main = putStrLn "Hello world"
```

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

### Install Idris 2 with Nix

Source: https://github.com/idris-lang/idris2/blob/main/INSTALL.md

Install Idris 2 using the Nix package manager. This is suitable for users who manage their environments with Nix.

```sh
nix-env -i idris2
```

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

### Build and Install Idris 2

Source: https://github.com/idris-lang/idris2/blob/main/docs/source/tutorial/windows.md

Compiles and installs Idris 2 after setting up the SCHEME environment variable. This command should be run from an MSYS2 shell after navigating to the Idris2 directory.

```bash
export SCHEME=scheme
make bootstrap && make install
```

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

### Rebind Names Locally

Source: https://github.com/idris-lang/idris2/blob/main/docs/source/updates/updates.md

Demonstrates how to locally rebind a name to resolve ambiguity, using `Prelude.(::)` as an example.

```idris
Main> let (::) = Prelude.(::) in [1,2,3]
```

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

### Example Usage of Show Nat

Source: https://github.com/idris-lang/idris2/blob/main/docs/source/tutorial/interfaces.md

Demonstrates the usage of the 'show' function for the 'Nat' type, converting a nested 'S' constructor to its string representation.

```text
Main> show (S (S (S Z)))
"sssZ" : String
```

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

### Install Idris 2 with Racket as the compiler

Source: https://github.com/idris-lang/idris2/blob/main/INSTALL.md

If you are building Idris 2 from source and using Racket as the Scheme compiler, append this environment variable to the install command.

```sh
IDRIS2_CG=racket make install
```

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

### C Code for FFI Example

Source: https://github.com/idris-lang/idris2/blob/main/docs/source/ffi/ffi.md

This C code defines two functions: `add` for simple integer addition and `addWithMessage` which prints a message before returning the sum. These are used as examples for calling C from Idris.

```c
#include <stdio.h>

int add(int x, int y) {
    return x+y;
}

int addWithMessage(char* msg, int x, int y) {
    printf("%s: %d + %d = %d\n", msg, x, y, x+y);
    return x+y;
}
```

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

### Do Notation Example: Sequencing Computations

Source: https://github.com/idris-lang/idris2/blob/main/docs/source/typedd/typedd.md

Illustrates how a do block without binding (<-) is desugared into chained >> operations for sequencing computations.

```idris
do
  foo
  bar
  baz
```

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

### Start Idris 2 Interpreter

Source: https://github.com/idris-lang/idris2/blob/main/docs/source/listing/idris-prompt-interp.txt

To start the Idris 2 interpreter, run the command 'idris2 interp.idr' in your terminal. This will load the specified Idris file and present the interactive prompt.

```bash
$ idris2 interp.idr
     ____    __     _         ___ 
    /  _/___/ /____(_)____   |__ \
    / // __  / ___/ / ___/   __/ /     Version 0.8.0
  _/ // /_/ / /  / (__  )   / __/      https://www.idris-lang.org
 /___/\__,_/_/  /_/____/   /____/      Type :? for help

Welcome to Idris 2.  Enjoy yourself!
Main>
```

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

### Use an Installed Idris Package

Source: https://github.com/idris-lang/idris2/blob/main/docs/source/tutorial/packages.md

Specify an installed package using the --package (or -p) option followed by the package name when compiling a main module.

```default
idris2 -p maths Main.idr
```

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

### Compile Code with the Custom Backend

Source: https://github.com/idris-lang/idris2/blob/main/docs/source/backends/custom.md

Use the custom backend to compile a file. This example shows how to invoke the 'lazy' codegen and specifies the output executable name.

```shell
$ ./build/exec/lazy-idris2 --cg lazy Hello.idr -o hello
```

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

### Unbound Implicit Example

Source: https://github.com/idris-lang/idris2/blob/main/docs/source/implementation/overview.md

Demonstrates how unbound implicits are elaborated into holes and then converted to implicit pi bindings. It also shows how additional names can be inferred.

```idris
map : {f : _} -> (a -> b) -> f a -> f b
```

```idris
map : {f : _} -> {0 a : _} -> {0 b : _} -> (a -> b) -> f a -> f b
```

```idris
lookup : HasType i xs t -> Env xs -> t
```

```idris
lookup : forall i, x, t . HasType i xs t -> Env xs -> t
```

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

### Example Usage of `rewrite`

Source: https://github.com/idris-lang/idris2/blob/main/docs/source/proofs/propositional.md

Demonstrates using `rewrite` with `y=x` and `p1 x` to prove `p1 y`. The property `p1` is defined as `x=2`.

```idris
p1: Nat -> Type
p1 x = (x=2)
```

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

### Prove Simple Equalities in Idris

Source: https://github.com/idris-lang/idris2/blob/main/docs/source/tutorial/theorems.md

Demonstrates proving simple, self-evident equalities using the `Refl` constructor. These examples show how to assert that a value is equal to itself.

```idris
fiveIsFive : 5 = 5
fiveIsFive = Refl

twoPlusTwo : 2 + 2 = 4
twoPlusTwo = Refl
```

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

### Example Usage of Map with Vect

Source: https://github.com/idris-lang/idris2/blob/main/docs/source/tutorial/typesfuns.md

Demonstrates using the map function to double each element in a Vect of integers.

```default
*UsefulTypes> show (map double intVec)
"[2, 4, 6, 8, 10]" : String
```

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

### Example Usage of Lambda Calculus Parser

Source: https://github.com/idris-lang/idris2/blob/main/docs/source/cookbook/parsing.md

Demonstrates how to use the `parse` function to parse a lambda calculus expression string and print the resulting abstract syntax tree.

```text
$ idris2 -p contrib LambdaCalculus.idr
Main> :exec printLn $ parse "let name = world in (\\x.hello x) name"
Right (let name = world in (\x.hello x) name)
```

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

### Complete Example: Initialize, Update, Display, and Free 'Point'

Source: https://github.com/idris-lang/idris2/blob/main/docs/source/ffi/ffi.md

A complete Idris 'main' function demonstrating the lifecycle of a 'Point' struct: creation, field update, display, and freeing.

```idris
main : IO ()
main = do let pt = mkPoint 20 30
          setField pt "x" (the Int 40)
          putStrLn $ showPoint pt
          freePoint pt
```

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

### Implicit Arguments in Idris 2 Types

Source: https://github.com/idris-lang/idris2/blob/main/docs/source/updates/updates.md

In Idris, names starting with a lowercase letter are implicitly bound in types. This example shows 'n', 'a', and 'm' as implicitly bound arguments.

```idris
append : Vect n a -> Vect m a -> Vect (n + m) a
append xs ys = ?append_rhs
```

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

### Write a 'Hello, World!' program in Idris2

Source: https://github.com/idris-lang/idris2/blob/main/www/source/index.md

This is a basic Idris2 program that prints a greeting to the console. It requires the 'IO' monad for side effects. You can run this example using the `--exec ENTRYPOINT` option.

```idris
module Main

||| My first Idris2 function
main : IO ()
main = putStrLn "Hello, and welcome to Idris2!"
```

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

### Idris Basic Completion Function Example

Source: https://github.com/idris-lang/idris2/blob/main/docs/source/ffi/readline.md

A simple Idris function that always returns 'hamster' as a completion for the first call, and Nothing for subsequent calls. Used for testing the completion setup.

```idris
testComplete : String -> Int -> IO (Maybe String)
testComplete text 0 = pure $ Just "hamster"
testComplete text st = pure Nothing
```

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

### Example of Monadic Addition with a Nothing Value

Source: https://github.com/idris-lang/idris2/blob/main/docs/source/tutorial/interfaces.md

Demonstrates the `m_add` function with one `Just` value and one `Nothing` value, showing the failure propagation.

```default
Main> m_add (Just 82) Nothing
Nothing
```

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

### Example Interpreter Usage (Failure)

Source: https://github.com/idris-lang/idris2/blob/main/docs/source/tutorial/interfaces.md

Demonstrates a failed evaluation of an arithmetic expression due to an undefined variable using the runEval function.

```default
InterpE> runEval [("x", 10), ("y",84)] (Add (Var "x") (Var "z"))
Nothing
```

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

### Build a Package

Source: https://github.com/idris-lang/idris2/blob/main/docs/source/reference/packages.md

Command to build all modules defined in the 'test.ipkg' package file.

```bash
idris2 --build test.ipkg
```

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

### Start IDE Mode on Specific Socket

Source: https://github.com/idris-lang/idris2/blob/main/docs/source/implementation/ide-protocol.md

Initiates IDE mode on a specified hostname and port. This allows for predictable socket connections for IDE integration.

```default
idris2 --ide-mode-socket localhost:12345
12345
```

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

### Example Usage of lookup_default

Source: https://github.com/idris-lang/idris2/blob/main/docs/source/tutorial/typesfuns.md

Demonstrates the behavior of the `lookup_default` function with both in-bounds and out-of-bounds indices, showing the returned value or the default value.

```default
*UsefulTypes> lookup_default 2 [3,4,5,6] (-1)
5 : Integer
*UsefulTypes> lookup_default 4 [3,4,5,6] (-1)
-1 : Integer
```

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

### App Program with State Management

Source: https://github.com/idris-lang/idris2/blob/main/docs/source/app/introapp.md

An example of an App program that includes state management (Counter) alongside console IO. Requires Console and State interfaces.

```idris
data Counter : Type where

helloCount : (Console es, State Counter Int es) => App es ()
helloCount = do c <- get Counter
                put Counter (c + 1)
                putStrLn "Hello, counting world"
                c <- get Counter
                putStrLn ("Counter " ++ show c)
```

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

### Library Package Description

Source: https://github.com/idris-lang/idris2/blob/main/docs/source/reference/packages.md

Defines a library package named 'test' with version 0.0.1 and modules Foo and Bar. When installed, it will reside in a directory named 'test-0.1'.

```default
package test
version = 0.0.1

modules = Foo, Bar
```

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

### Idris 2 Quicksort (Untotal)

Source: https://github.com/idris-lang/idris2/blob/main/docs/source/tutorial/theorems.md

This is an example of a quicksort implementation that Idris 2 cannot automatically verify as total because it cannot determine that the filtered lists are smaller than the original.

```idris
qsort : Ord a => List a -> List a
qsort [] = []
qsort (x :: xs)
   = qsort (filter (< x) xs) ++ 
      (x :: qsort (filter (>= x) xs))
```

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

### FileIO Implementation with PrimIO and Exception Handling

Source: https://github.com/idris-lang/idris2/blob/main/docs/source/app/interfaces.md

Provides an example implementation of the FileIO interface, leveraging PrimIO for primitive operations and catch for exception handling. This demonstrates how to bridge primitive IO with the abstract interface.

```idris
Has [PrimIO, Exception IOError] e => FileIO e where
  withFile fname m onError proc
      = do Right h <- primIO $ openFile fname m
              | Left err => onError (FileErr (toFileEx err))
           res <- catch (proc h) onError
           primIO $ closeFile h
           pure res
  ...
```

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

### Build compile-chez-program-tool

Source: https://github.com/idris-lang/idris2/blob/main/docs/source/backends/chez.md

Build the compile-chez-program-tool by running the configuration script with the Chez Scheme bootpath, followed by 'make'.

```default
$ scheme --script gen-config.ss --bootpath <bootpath>
```

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

### Install Idris 2 Docs Dependencies with Pip

Source: https://github.com/idris-lang/idris2/blob/main/docs/README.md

Installs necessary dependencies for building Idris 2 documentation using pip within a virtual environment. Ensure you have Python and pip installed.

```sh
python3 -m venv idris2docs_venv
source idris2docs_venv/bin/activate
pip install --upgrade pip
pip install sphinx_rtd_theme myst-parser sphinx sphinx-book-theme sphinxcontrib-bibtex sphinx-copybutton
```

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

### Intro

Source: https://github.com/idris-lang/idris2/blob/main/docs/source/implementation/ide-protocol.md

Returns a list of valid saturated constructors that can be used in a hole.

```APIDOC
## :intro LINE NAME

### Description
Returns the non-empty list of valid saturated constructors that can be used in the hole
at line `LINE` named `NAME`.

### Parameters
#### Path Parameters
- **LINE** (integer) - Required - The line number of the hole.
- **NAME** (string) - Required - The name of the hole.
```

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

### Record Update Syntax Examples

Source: https://github.com/idris-lang/idris2/blob/main/docs/source/reference/records.md

Demonstrates the new dot-syntax for record updates, including assignment (`:=`) and update-with-function (`$=`) operators, and shows compatibility with the older arrow-style syntax.

```idris
-- record update syntax uses dots now
  -- prints 3.0
  printLn $ ({ topLeft.x := 3 } rect).topLeft.x

  -- but for compatibility, we support the old syntax, too
  printLn $ ({ topLeft->x := 3 } rect).topLeft.x

  -- prints 2.1
  printLn $ ({ topLeft.x $= (+1) } rect).topLeft.x
  printLn $ ({ topLeft->x $= (+1) } rect).topLeft.x
```

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

### Running Idris 2 Hello World

Source: https://github.com/idris-lang/idris2/blob/main/docs/source/listing/idris-prompt-helloworld.txt

Execute a basic Idris program from the command line. This involves saving the code to a file and then running it using the idris2 executable.

```bash
$ idris2 hello.idr
     ____    __     _         ___ 
    /  _/___/ /____(_)____   |__ \
    / // __  / ___/ / ___/   __/ /     Version 0.8.0
  _/ // /_/ / /  / (__  )   / __/      https://www.idris-lang.org
 /___/\__,_/_/  /_/____/   /____/      Type :? for help

Welcome to Idris 2.  Enjoy yourself!
Main> :t main
Main.main : IO ()
Main> :c hello main
File build/exec/hello written
Main> :q
Bye for now!
```

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

### Idris Counter Type Example

Source: https://github.com/idris-lang/idris2/blob/main/docs/source/app/exceptionsstate.md

An example of a type that can be used as a tag for state management, such as `Counter`.

```idris
data Counter : Type where -- complete definition
```

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

### Complete App Program with IO

Source: https://github.com/idris-lang/idris2/blob/main/docs/source/app/introapp.md

Shows how to define and run a complete App program within the IO monad. Imports necessary modules.

```idris
module Main

import Control.App
import Control.App.Console

hello : Console es => App es ()
hello = putStrLn "Hello, App world!"

main : IO ()
main = run hello
```

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

### Module Re-export Example

Source: https://github.com/idris-lang/idris2/blob/main/docs/source/tutorial/modules.md

Demonstrates how to re-export a module using `import public`. Module A will export its own names and public/abstract names from module C, but not from module B.

```default
module A

import B
import public C
```

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

### Generate Package Documentation

Source: https://github.com/idris-lang/idris2/blob/main/docs/source/reference/packages.md

Command to generate HTML documentation for the 'test.ipkg' package, outputting to the 'build/docs' directory.

```bash
idris2 --mkdoc test.ipkg
```

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

### Idris Example: Using C Function with Callback

Source: https://github.com/idris-lang/idris2/blob/main/docs/source/ffi/ffi.md

Demonstrates calling the Idris wrapper for 'applyFn' with a custom Idris callback function 'pluralise'. It prints the results.

```idris
pluralise : String -> Int -> String
pluralise str x
    = show x ++ " " ++
             if x == 1
                then str
                else str ++ "s"

main : IO ()
main
    = do str1 <- applyFn "Biscuit" 10 pluralise
         putStrLn str1
         str2 <- applyFn "Tree" 1 pluralise
         putStrLn str2
```

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

### Idris2 Literate Comment Example

Source: https://github.com/idris-lang/idris2/blob/main/tests/idris2/literate/literate010/MyFirstIdrisProgram.org

Demonstrates an active code line using the #+IDRIS: directive within an org-mode example block.

```idris
#+IDRIS: %name Vect xs, ys
```

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

### Main Function to Run Store Program

Source: https://github.com/idris-lang/idris2/blob/main/docs/source/app/linear.md

The main entry point of the application, which runs the `storeProg` using `run`.

```idris
main : IO ()
main = run storeProg
```

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

### Idris: Examples of Non-Total Functions

Source: https://github.com/idris-lang/idris2/blob/main/docs/source/tutorial/theorems.md

These examples demonstrate functions that are not total, either because they are partially defined or do not terminate. Use `:total` to check their status.

```idris
-- making use of 'hd' being partially defined
empty1 : Void
empty1 = hd [] where
    hd : List a -> a
    hd (x :: xs) = x

-- not terminating
empty2 : Void
empty2 = empty2
```

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

### Create and Initialize a Record Instance

Source: https://github.com/idris-lang/idris2/blob/main/docs/source/tutorial/typesfuns.md

Creates an instance of the 'Person' record using its constructor 'MkPerson' and provides values for all fields.

```idris
fred : Person
fred = MkPerson "Fred" "Joe" "Bloggs" 30
```

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

### Zsh Auto-completion Setup

Source: https://github.com/idris-lang/idris2/blob/main/INSTALL.md

Configure tab auto-completion for Idris 2 in Zsh shells using bashcompinit. Add the command to your .zshrc for persistent setup.

```zsh
eval "$(idris2 --zsh-completion-script idris2)"
```

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

### Get and Put State in Idris

Source: https://github.com/idris-lang/idris2/blob/main/docs/source/app/exceptionsstate.md

Functions to access (`get`) and update (`put`) application state. They use an `auto`-implicit with a `tag` to implicitly pass the relevant `State`.

```idris
get : (0 tag : _) -> State tag t e => App {l} e t
put : (0 tag : _) -> State tag t e => (1 val : t) -> App {l} e ()
```

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

### Idris 2 Sum of Lengths - Error Example

Source: https://github.com/idris-lang/idris2/blob/main/docs/source/tutorial/multiplicities.md

This example shows an error in Idris 2 when trying to sum lengths of vectors where 'm' is not available at runtime because it has multiplicity '0'.

```idris
sumLengths : Vect m a -> Vect n a —> Nat
sumLengths xs ys = vlen xs + vlen ys
```

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

### Running App with Initialized State

Source: https://github.com/idris-lang/idris2/blob/main/docs/source/app/introapp.md

Demonstrates how to run an App program that requires state initialization. The 'new' function is used to provide an initial value for the state.

```idris
main : IO ()
main = run (new 93 helloCount)
```

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

### Interactive Readline Loop Example

Source: https://github.com/idris-lang/idris2/blob/main/docs/source/ffi/readline.md

An example Idris program demonstrating the use of the safe readline API and addHistory function. It reads input, echoes it, records non-empty inputs in history, and exits on 'quit'.

```Idris
echoLoop : IO ()
echoLoop
    = do Just x <- readline "> "
              | Nothing => putStrLn "EOF"
         putStrLn ("Read: " ++ x)
         when (x /= "") $ addHistory x
         if x /= "quit"
            then echoLoop
            else putStrLn "Done"
```

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

### Interactive Door Protocol Development

Source: https://github.com/idris-lang/idris2/blob/main/docs/source/tutorial/multiplicities.md

Demonstrates building a door protocol interactively. This snippet shows a point where the type of `?whatnow` can be checked to observe the changing multiplicities of door variables.

```idris
doorProg : IO ()
doorProg
    = newDoor $ \d =>
          let d' = openDoor d in
              ?whatnow
```

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

### Linearity Annotation Example in Idris 2

Source: https://github.com/idris-lang/idris2/blob/main/docs/source/faq/faq.md

Illustrates a linear function annotation in Idris 2. This example shows how precise usage information can be specified, but also highlights potential conflicts with functions that do not guarantee linearity.

```default
id : (1 _ : a) -> a
id x = x
```

```default
map : (a -> b) -> List a -> List b
```

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

### Example IDE Protocol Interaction

Source: https://github.com/idris-lang/idris2/blob/main/docs/source/implementation/ide-protocol.md

Demonstrates a typical interaction sequence on the wire, including loading a file, receiving status messages, and the final return status. Each message is prefixed with its length in hexadecimal.

```default
00002a((:load-file "/home/hannes/empty.idr") 1)
000039(:write-string "Type checking /home/hannes/empty.idr" 1)
000025(:set-prompt "/home/hannes/empty" 1)
000032(:return (:ok "Loaded /home/hannes/empty.idr") 1)
```

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

### Infinite Stream of Ones

Source: https://github.com/idris-lang/idris2/blob/main/docs/source/tutorial/typesfuns.md

An example of creating an infinite stream of ones using the Stream data type.

```idris
ones : Stream Nat
ones = 1 :: ones
```

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

### Get Type of a Prefix Field Projection

Source: https://github.com/idris-lang/idris2/blob/main/docs/source/tutorial/typesfuns.md

Shows how to check the type of a prefix field projection function.

```default
*Record> :t firstName
firstName : Person -> String
```

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

### Eager Evaluation Example

Source: https://github.com/idris-lang/idris2/blob/main/docs/source/tutorial/typesfuns.md

Demonstrates Idris's default eager evaluation where all arguments are evaluated before function execution.

```idris
ifThenElse : Bool -> a -> a -> a
ifThenElse True  t e = t
ifThenElse False t e = e
```

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

### Natural Number Compilation Example

Source: https://github.com/idris-lang/idris2/blob/main/docs/source/reference/builtins.md

Illustrates the compilation of natural number constructors 'Zero' and 'Succ' into their optimized Integer representations. 'Zero' becomes 0, and 'Succ k' becomes 1 + k.

```idris
case k of
    Z => zexp
    S k' => sexp
```

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

### Term Manipulation Functions

Source: https://github.com/idris-lang/idris2/blob/main/docs/source/implementation/overview.md

Provides examples of handy tools for manipulating terms with their indices, such as 'weaken', 'embed', and 'refToLocal'.

```idris
weaken : Term vars -> Term (n :: vars) -- actually in an interface, Weaken
```

```idris
embed : Term vars -> Term (ns ++ vars)
```

```idris
refToLocal : (x : Name) -> -- explicit name of a reference
             (new : Name) -> -- name to bind as
             Term vars -> Term (new :: vars)
```

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

### Run Idris 2 with the Custom Backend

Source: https://github.com/idris-lang/idris2/blob/main/docs/source/backends/custom.md

Execute the Idris 2 binary that includes the custom backend. This demonstrates the interactive session with the new codegen available.

```shell
$ ./build/exec/lazy-idris2
     ____    __     _         ___ 
    /  _/___/ /____(_)____   |__ \
    / // __  / ___/ / ___/   __/ /
  _/ // /_/ / /  / (__  )   / __/      Version 0.2.0-bd9498c00
 /___/\__,_/_/  /_/____/   /____/      https://www.idris-lang.org
    Type :? for help

Welcome to Idris 2.  Enjoy yourself!
With codegen for: lazy
Main>
```

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

### Basic Operator Usage

Source: https://github.com/idris-lang/idris2/blob/main/docs/source/reference/operators.md

Demonstrates the equivalence between infix operator usage and function application with parentheses. This is useful for understanding how operators are parsed.

```idris
1 + 3
(+) 1 3
```

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

### REPL Type Query for Ord

Source: https://github.com/idris-lang/idris2/blob/main/docs/source/tutorial/interfaces.md

An example from the REPL showing the type of the Ord constraint, illustrating that constraints are first-class objects.

```default
Main> :t Ord
Prelude.Ord : Type -> Type
```

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

### Nested `with` Rule in Idris

Source: https://github.com/idris-lang/idris2/blob/main/docs/source/tutorial/views.md

Illustrates nested `with` clauses in Idris. This example shows how multiple intermediate computations can be matched sequentially.

```idris
foo : Int -> Int -> Bool
foo n m with (n + 1)
  foo _ m | 2 with (m + 1)
    foo _ _ | 2 | 3 = True
    foo _ _ | 2 | _ = False
  foo _ _ | _ = False
```

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

### Idris 2 Hole Context with Let Bindings Displayed

Source: https://github.com/idris-lang/idris2/wiki/What-Contributions-are-Needed

Illustrates the expected display of local `let` bindings within a hole's context in Idris 2. This example shows `n` and `k` as available variables.

```idris
Main> :t hole
   n : Nat
   k : Nat
-------------------------------------
hole : Nat
```

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

### Documenting a Simple Datatype in Idris

Source: https://github.com/idris-lang/idris2/blob/main/docs/source/reference/documenting.md

Inline documentation for a simple datatype `Ty` with constructors `UNIT` and `ARR`. Each constructor can also be documented.

```idris
||| Here's a simple datatype
data Ty = 
  ||| Unit
  UNIT |
  ||| Functions
  ARR Ty Ty
```

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

### Idris `do`-notation for Sequencing I/O Actions

Source: https://github.com/idris-lang/idris2/blob/main/docs/source/tutorial/typesfuns.md

Demonstrates sequencing I/O actions using `do`-notation. The `<-` syntax extracts the result from an `IO` action into a variable. Indentation is significant.

```idris
greet : IO ()
greet = do putStr "What is your name? "
           name <- getLine
           putStrLn ("Hello " ++ name)
```

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

### Secure Data Store Program with bindL

Source: https://github.com/idris-lang/idris2/blob/main/docs/source/app/linear.md

A complete program demonstrating secure data store access using `bindL` for linear sequencing. It handles login, reading secrets, and logout, ensuring linear resource usage.

```idris
storeProg : Has [Console, StoreI] e => App e ()
storeProg = let (>>=) = bindL
                (>>) = seqL in
      do putStr "Password: "
         password <- getStr
         connect $ \s ->
           do let True # s = login s password
                | False # s => do putStrLn "Wrong password"
                                  disconnect s
              let str # s = readSecret s
              putStrLn $ "Secret: " ++ show str
              let s = logout s
              disconnect s
```

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

### Visible LaTeX Code Block

Source: https://github.com/idris-lang/idris2/blob/main/docs/source/reference/literate.md

Example of a visible code block within a LaTeX literate file using the 'code' environment.

```default
\begin{code}
data Nat = Z | S Nat
\end{code}
```

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

### Precedence Example

Source: https://github.com/idris-lang/idris2/blob/main/docs/source/reference/operators.md

Declares '*' with a higher precedence (9) than '+' (implicitly 8). This ensures `n + m * x` is parsed as `n + (m * x)`.

```idris
infixl 9 *
infixl 8 +
```

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

### Make With

Source: https://github.com/idris-lang/idris2/blob/main/docs/source/implementation/ide-protocol.md

Creates a with-rule pattern match template for a function clause.

```APIDOC
## :make-with LINE NAME

### Description
Create a with-rule pattern match template for the clause of function `NAME` on line `LINE`.
The new code is returned with no highlighting.

### Parameters
#### Path Parameters
- **LINE** (integer) - Required - The program line number.
- **NAME** (string) - Required - The name of the function.
```

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

### Basic `main` I/O Program

Source: https://github.com/idris-lang/idris2/blob/main/docs/source/tutorial/typesfuns.md

A simple I/O program demonstrating the `main` function, which has the type `IO ()`, indicating an I/O action with no specific return value.

```idris
main : IO ()
main = putStrLn "Hello world"
```

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

### Node.js File Size Foreign Function

Source: https://github.com/idris-lang/idris2/blob/main/docs/source/backends/javascript.md

Defines a foreign function to get the size of a file in Node.js using require('fs').

```Idris
%foreign "node:lambda:fp=>require('fs').fstatSync(fp.fd, {bigint: false}).size"
prim__fileSize : FilePtr -> PrimIO Int
```

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

### Proving plus n Z = n with Case Analysis

Source: https://github.com/idris-lang/idris2/blob/main/docs/source/proofs/propositional.md

Demonstrates proving `plus n Z = n` by handling base and recursive cases separately. Requires explicit handling for `Z` and `S k`.

```idris
plusReducesR : (n : Nat) -> plus n Z = n
plusReducesR Z = Refl
plusReducesR (S k)
    = let rec = plusReducesR k in
          rewrite rec in Refl
```