### Install Dependencies, Build, and Start Development Server

Source: https://github.com/intersectmbo/plutus/blob/master/doc/docusaurus/README.md

Use these yarn commands to manage the Docusaurus website. Run `yarn build` to create a production build and `yarn start` for live development.

```bash
yarn # to install dependencies 
yarn build # to build the website 
yarn start # for live development on localhost
```

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

### Example Agda Library Path List

Source: https://github.com/intersectmbo/plutus/blob/master/plutus-metatheory/AGDA.md

Illustrates the format of the $AGDA_DIR/libraries file, which lists the paths to installed .agda-lib files. Ensure these paths are correct for Agda to find libraries.

```text
/nix/store/j56804kxj67326j0llc3isrr8njxqlw3-standard-library-2.1.1/standard-library.agda-lib
/Users/me/plutus-metatheory.agda-lib
/some/other.agda-lib
```

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

### Alternative Extrinsic Setup

Source: https://github.com/intersectmbo/plutus/blob/master/plutus-metatheory/src/VerifiedCompilation/UCaseReduce.lagda.md

Illustrates an alternative, more extrinsic setup for reduction functions, noting it requires more boilerplate.

```text
red-unit : X ⊢ → Maybe (X ⊢)

red-unit-sound : (M M' : X ⊢) → red-unit M ≡ just M' → CaseUnit R M M'
```

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

### Start Local HTTP Server (Python 3)

Source: https://github.com/intersectmbo/plutus/blob/master/doc/cost-models/index.html

Alternative command to start a local HTTP server using Python 3.

```bash
python3 -m http.server 8000
```

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

### Install Dependencies for Off-Chain Code

Source: https://github.com/intersectmbo/plutus/blob/master/doc/docusaurus/docs/auction-smart-contract/end-to-end/generating-keys.md

Installs the Mesh SDK, Harmonic Labs Pair, and CBOR for off-chain operations. Ensure Node.js and Yarn are installed.

```bash
git clone git@github.com:IntersectMBO/plinth-template.git on-chain
mkdir off-chain && cd $_
yarn init -y
yarn add @meshsdk/core
yarn add @harmoniclabs/pair
yarn add cbor
```

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

### State Initialization Example

Source: https://github.com/intersectmbo/plutus/blob/master/plutus-metatheory/src/Algorithmic/BehaviouralEquivalence/CCvsCK.lagda.md

An example demonstrating the initialization of a state with a specific value, likely for testing or setting up a scenario in Plutus.

```agda
test : State (con (ne (^ (atomic aUnit))))
test = ε ▻ (ƛ (con tt refl) · (builtin iData / refl · con (+ 0) refl))
```

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

### Start Local HTTP Server

Source: https://github.com/intersectmbo/plutus/blob/master/doc/cost-models/README.md

Use this command to start a local HTTP server for development. Access the visualizations by opening http://localhost:8000/ in your browser.

```bash
python -m http.server 8000
```

```bash
python3 -m http.server 8000
```

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

### UPLC Constructor Example

Source: https://github.com/intersectmbo/plutus/blob/master/plutus-benchmark/uplc-evaluator/SPEC.md

An example of a UPLC program evaluating to a constructor with tag and fields. Requires UPLC version 1.1.0 or higher.

```uplc
(program 1.1.0
  (constr 0 (con integer 42) (con bool True))
)
```

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

### Plutus IR Example: Implementing fromMaybe

Source: https://github.com/intersectmbo/plutus/blob/master/doc/notes/plutus-ir/plutus-ir.md

Provides an example of implementing the `fromMaybe` function in Plutus IR. It showcases the definition of a `Maybe` datatype and its usage with pattern matching.

```haskell
# bind Maybe
(let (nonrec)
    (datatypebind
        (datatype
            (tyvardecl Maybe (fun (type) (type)))
            (tyvardecl a (type))
            match_Maybe
            (vardecl
                Nothing
                [Maybe a]
            )
            (vardecl
                Just
                (fun a [Maybe a])
            )
        )
    )
    (abs a (type)
        (lam default a
            (lam arg [Maybe a]
                # match on the arg, producing an a, giving the default
                # in the Nothing case and using the identity function
                # in the Just case
                [ { match_Maybe a } arg default (lam x a x) ]
            )
        )
    )
)
```

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

### Example: Nested abstractions and applications

Source: https://github.com/intersectmbo/plutus/blob/master/plutus-metatheory/src/VerifiedCompilation/UForceDelay.lagda.md

Demonstrates the translation of deeply nested lambda abstractions and applications with `force` and `delay`. This complex example uses a combination of `translationfd`, `pushfd`, `forcedelay`, and `TransMatch` constructors to handle the nested structure.

```Agda
_ : pureFD {1} (force (force (ƛ (ƛ (delay (delay (` zero))) · (` zero)) · (` zero)))) (ƛ (ƛ (` zero) · (` zero)) · (` zero))
_ = (translationfd (Translation.match (TransMatch.force (Translation.istranslation (pushfd (translationfd reflexive) (translationfd reflexive)))))) ⨾ ((translationfd (Translation.match (TransMatch.force (Translation.match (TransMatch.app (Translation.match (TransMatch.ƛ (Translation.istranslation (pushfd (translationfd reflexive) (translationfd reflexive))))) reflexive))))) ⨾ ( pushfd (translationfd reflexive) (translationfd reflexive) ⨾ ((translationfd (Translation.match (TransMatch.app (Translation.match (TransMatch.ƛ (Translation.match (TransMatch.app (Translation.match (TransMatch.ƛ (Translation.istranslation ((translationfd (Translation.match (TransMatch.force (Translation.istranslation (forcedelay (translationfd (Translation.match (TransMatch.delay (Translation.match TransMatch.var))))))))) ⨾ (forcedelay (translationfd (Translation.match TransMatch.var))))))) reflexive)))) reflexive))))))
```

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

### Plutus Core Example of Empty List of Integers

Source: https://github.com/intersectmbo/plutus/blob/master/doc/notes/fomega/deep-isorecursive/problem.md

Demonstrates the construction of an empty list of integers using the 'wrap' construct according to the defined Plutus Core rules. This example highlights the type inference challenge.

```plutus-core
wrap List
    (\(A :: *) -> all (R :: *). R -> (A -> List A -> R) -> R)
    (/\(R :: *) -> \(z : R) (f : Integer -> List Integer -> R) -> z)

```

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

### Haskell Constraints: Good Example

Source: https://github.com/intersectmbo/plutus/blob/master/STYLEGUIDE.adoc

Shows the correct way to write multiple constraints in a type signature by uncurrying them.

```Haskell
foo :: (Eq a, Ord a) => a -> a -> a

```

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

### Example: force ((ƛ (delay zero)) · zero) translation

Source: https://github.com/intersectmbo/plutus/blob/master/plutus-metatheory/src/VerifiedCompilation/UForceDelay.lagda.md

Illustrates a more complex translation involving lambda abstraction and application. This example uses `pushfd`, `translationfd`, `reflexive`, and `TransMatch.delay` to show the cancellation of `force` and `delay` within an application.

```Agda
forceappdelay : pureFD {1} (force ((ƛ (delay (` zero))) · (` zero))) ((ƛ (` zero)) · (` zero))
forceappdelay = (pushfd (translationfd (Translation.match 
                                         (TransMatch.delay (Translation.match TransMatch.var)))) (translationfd reflexive)) ⨾ (translationfd (Translation.match (TransMatch.app (Translation.match (TransMatch.ƛ (Translation.istranslation 
                                                                                                                                                          (forcedelay (translationfd (Translation.match TransMatch.var)))))) (Translation.match TransMatch.var))))
```

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

### Example PlutusV3 Configuration with Custom Mainnet Cost Model

Source: https://github.com/intersectmbo/plutus/blob/master/plutus-benchmark/uplc-evaluator/SPEC.md

This JSON object shows an example configuration for the Plutus UPLC evaluator using PlutusV3 with custom mainnet cost model parameters. It specifies the protocol version, ledger language, UPLC version, and the array of cost model parameters.

```json
{
  "protocol_version": 10,
  "ledger_language": "PlutusV3",
  "uplc_version": "1.1.0",
  "cost_model_params": [
    100788, 420, 1, 1, 1000, 173, 0, 1, 1000, 59957, 4, 1, 11183, 32,
    201305, 8356, 4, 16000, 100, 16000, 100, 16000, 100, 16000, 100,
    16000, 100, 16000, 100, 100, 100, 16000, 100, 94375, 32, 132994, 32,
    61462, 4, 72010, 178, 0, 1, 22151, 32, 91189, 769, 4, 2,
    85848, 123203, 7305, -900, 1716, 549, 57, 85848, 0, 1, 1, 1000,
    42921, 4, 2, 24548, 29498, 38, 1, 898148, 27279, 1, 51775, 558,
    1, 39184, 1000, 60594, 1, 141895, 32, 83150, 32, 15299, 32, 76049,
    1, 13169, 4, 22100, 10, 28999, 74, 1, 28999, 74, 1, 43285, 552,
    1, 44749, 541, 1, 33852, 32, 68246, 32, 72362, 32, 7243, 32,
    7391, 32, 11546, 32, 85848, 123203, 7305, -900, 1716, 549, 57,
    85848, 0, 1, 90434, 519, 0, 1, 74433, 32, 85848, 123203, 7305,
    -900, 1716, 549, 57, 85848, 0, 1, 1, 85848, 123203, 7305, -900,
    1716, 549, 57, 85848, 0, 1, 955506, 213312, 0, 2, 270652, 22588,
    4, 1457325, 64566, 4, 20467, 1, 4, 0, 141992, 32, 100788, 420,
    1, 1, 81663, 32, 59498, 32, 20142, 32, 24588, 32, 20744, 32,
    25933, 32, 24623, 32, 43053543, 10, 53384111, 14333, 10, 43574283,
    26308, 10, 16000, 100, 16000, 100, 962335, 18, 2780678, 6, 442008,
    1, 52538055, 3756, 18, 267929, 18, 76433006, 8868, 18, 52948122,
    18, 1995836, 36, 3227919, 12, 901022, 1, 166917843, 4307, 36,
    284546, 36, 158221314, 26549, 36, 74698472, 36, 333849714, 1,
    254006273, 72, 2174038, 72, 2261318, 64571, 4, 207616, 8310, 4,
    1293828, 28716, 63, 0, 1, 1006041, 43623, 251, 0, 1
  ]
}
```

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

### SSH Config File Setup

Source: https://github.com/intersectmbo/plutus/blob/master/plutus-benchmark/uplc-evaluator/SPEC.md

Configure SSH to use an alias for the benchmarking server, simplifying connection commands.

```sshconfig
Host plutus-benchmarking
    HostName benchmarking.plutus.internal
    Port 22
    User benchmarking
    IdentityFile ~/.ssh/id_ed25519_plutus
    ServerAliveInterval 60
    ServerAliveCountMax 3
```

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

### Imaginary Plutus Tx Program

Source: https://github.com/intersectmbo/plutus/blob/master/plutus-core/docs/Typechecking PIR.md

An example of an imaginary Plutus Tx program that might not be directly writable but serves as a conceptual starting point.

```haskell
data Success = MkSuccess
MkSuccess
```

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

### Submit UPLC Program with Different Configurations

Source: https://github.com/intersectmbo/plutus/blob/master/plutus-benchmark/uplc-evaluator/SPEC.md

Examples demonstrating how to submit UPLC programs with different file extensions and configuration files, including default, custom JSON, and protocol-specific configurations.

```bash
# Submit textual program with default configuration
./submit-program.sh my-program.uplc.txt

# Submit flat-encoded program with custom configuration
./submit-program.sh my-program.uplc.flat my-config.json

# Submit textual program with protocol v7 configuration
./submit-program.sh validator.uplc.txt protocol-v7-config.json
```

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

### Validator for blueprint example

Source: https://github.com/intersectmbo/plutus/blob/master/doc/docusaurus/docs/working-with-scripts/producing-a-blueprint.md

The example validator function for the Plutus contract.

```haskell
{-# INLINEABLE mkMyPolicy #-}
mkMyPolicy :: MyParams -> MyDatum -> MyRedeemer -> ScriptContext -> Bool
mkMyPolicy = undefined

-- BEGIN validator
-- END validator
```

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

### Example of makeBuiltinMeaning Usage

Source: https://github.com/intersectmbo/plutus/blob/master/plutus-core/docs/BuiltinsOverview.md

Demonstrates the practical usage of `makeBuiltinMeaning` by providing a simple Haskell denotation (an if-then-else expression) and its corresponding costing function.

```haskell
makeBuiltinMeaning
    (\b x y -> if b then x else y)
    (runCostingFunThreeArguments . paramIfThenElse)
```

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

### Plinth Code Example

Source: https://github.com/intersectmbo/plutus/blob/master/doc/docusaurus/docs/using-plinth/compiling-plinth.md

An example of a Plinth function that can be compiled. Ensure necessary imports are present.

```haskell
module A where

import qualified PlutusTx.Prelude as PlutusTx

myPlutusTxCode :: Integer -> Integer
myPlutusTxCode x = x PlutusTx.+ 1
```

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

### Prime20 CEK Node Type Counts

Source: https://github.com/intersectmbo/plutus/blob/master/doc/notes/plutus-core/cek-budgeting-profiling/CekProfiling.md

Statistics on the number of calls to different PLC node types within the Prime20 example during CEK evaluation. This example shows a higher proportion of builtin evaluations compared to validation examples.

```text
   7,334,166 calls to compute_cek
   5,692,258 calls to return_cek

   Var:     1,958,665
   Lam:     1,006,700
   Apply:   2,667,199
   Const:   374,748
   Delay:   349,664
   Force  : 357,859
   Builtin: 619,331
   Error  : 0
```

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

### Build Project Artifacts with Nix

Source: https://github.com/intersectmbo/plutus/blob/master/CONTRIBUTING.adoc

This command demonstrates how to build Haskell components using Nix. Replace SYSTEM and PACKAGE with your specific system architecture and the desired package name. Refer to the Nix README for building other artifacts.

```bash
nix build .#cabalProject.x86_64-linux.hsPkgs.plutus-core.components.library
```

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

### Bad Error Message Example

Source: https://github.com/intersectmbo/plutus/blob/master/plutus-benchmark/uplc-evaluator/SPEC.md

Shows an example of a poor error message that lacks specific details and actionable guidance.

```text
"Parse error: unexpected token at 5:23"
```

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

### List Available Benchmarks with Stack

Source: https://github.com/intersectmbo/plutus/blob/master/plutus-benchmark/nofib/README.md

Use this command to list all available nofib benchmarks when using `stack` for building.

```bash
stack bench plutus-benchmark:nofib --ba --list
```

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

### Successful Evaluation Workflow Example Paths

Source: https://github.com/intersectmbo/plutus/blob/master/plutus-benchmark/uplc-evaluator/SPEC.md

Illustrates the file paths involved in a successful evaluation, from submitting a textual program and optional configuration to receiving a result file.

```bash
/benchmarking/input/a1b2c3d4-e5f6-4789-a012-3456789abcde.uplc.txt
```

```bash
/benchmarking/input/a1b2c3d4-e5f6-4789-a012-3456789abcde.config.json
```

```bash
/benchmarking/output/a1b2c3d4-e5f6-4789-a012-3456789abcde.result.json
```

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

### Interface types for blueprint example

Source: https://github.com/intersectmbo/plutus/blob/master/doc/docusaurus/docs/working-with-scripts/producing-a-blueprint.md

Defines the types used for the example contract's interface, including parameters, datum, and redeemer.

```haskell
{-# INLINEABLE mkMyPolicy #-}
mkMyPolicy :: MyParams -> MyDatum -> MyRedeemer -> ScriptContext -> Bool
mkMyPolicy = undefined

-- BEGIN interface types
-- END interface types
```

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

### Test New Function Locally

Source: https://github.com/intersectmbo/plutus/blob/master/doc/cost-models/README.md

After adding a new function, use this command to start a local server and test it. Navigate to http://localhost:8000/myfunction/ to view the new visualization.

```bash
python -m http.server 8000
```

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

### Example Configuration: Protocol v10 with Mainnet Cost Model

Source: https://github.com/intersectmbo/plutus/blob/master/plutus-benchmark/uplc-evaluator/SPEC.md

This configuration uses Protocol version 10 (Plomin), PlutusV3 ledger language, UPLC version 1.1.0, and the default mainnet cost model.

```json
{
  "protocol_version": 10,
  "ledger_language": "PlutusV3",
  "uplc_version": "1.1.0",
  "cost_model_params": null
}
```

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

### jQuery AJAX Settings and Setup

Source: https://github.com/intersectmbo/plutus/blob/master/doc/notes/fomega/scott-encoding-benchmarks/results/benchmarks-with-default.html

Defines default AJAX settings and provides a method to extend them. Use `ajaxSetup` to configure global AJAX behavior.

```javascript
w.extend({active:0,lastModified:{},etag:{},ajaxSettings:{url:Ct.href,type:"GET",isLocal:Pt.test(Ct.protocol),global:!0,processData:!0,async:!0,contentType:"application/x-www-form-urlencoded; charset=UTF-8",accepts:{"*":$t,text:"text/plain",html:"text/html",xml:"application/xml, text/xml",json:"application/json, text/javascript"},contents:{xml:/\bxml\b/,html:/\bhtml/,json:/\bjson\b/},responseFields:{xml:"responseXML",text:"responseText",json:"responseJSON"},converters:{"* text":String,"text html":!0,"text json":JSON.parse,"text xml":w.parseXML},flatOptions:{url:!0,context:!0}},ajaxSetup:function(e,t){return t?zt(zt(e,w.ajaxSettings),t):zt(w.ajaxSettings,e)},ajaxPrefilter:Ft(It),ajaxTransport:Ft(Wt),ajax:function(t,n){
```

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

### Example Error Message

Source: https://github.com/intersectmbo/plutus/blob/master/plutus-benchmark/uplc-evaluator/SPEC.md

This example demonstrates a human-readable error message for a syntax error, providing specific location information and guidance for correction.

```json
{
  "program_id": "550e8400-e29b-41d4-a716-446655440000",
  "status": "error",
  "error_type": "syntax_error",
  "error_message": "Syntax error at line 3, column 15: Expected closing parenthesis ')' but found 'con'"
}
```

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

### Invalid Job ID Examples

Source: https://github.com/intersectmbo/plutus/blob/master/plutus-benchmark/uplc-evaluator/SPEC.md

Illustrates examples of invalid job identifiers that will be rejected by the service. These do not conform to the UUID v4 format or naming conventions.

```text
job-123                  # Not UUID format
```

```text
550e8400e29b41d4         # Missing hyphens
```

```text
550E8400-E29B-41D4-...   # Uppercase not recommended
```

```text
not-a-uuid               # Invalid format
```

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

### Example of Polymorphic Built-in Type Signature

Source: https://github.com/intersectmbo/plutus/blob/master/doc/notes/plutus-core/Builtins_Overview.md

This is an example of a disallowed polymorphic built-in function type signature. Polymorphism over built-in type operators is not permitted.

```haskell
forall f. f integer -> bool
```

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

### Example: Integer Construction and Reduction

Source: https://github.com/intersectmbo/plutus/blob/master/plutus-metatheory/src/Untyped/Reduction.lagda.md

Demonstrates the construction of an integer literal and its reduction to a canonical form using beta-reduction and transitivity.

```lagda
open import RawU using (tag2TyTag; tmCon)
open import Data.Nat using (ℕ)
open import Agda.Builtin.Int using (Int)

integer : RawU.TyTag
integer = tag2TyTag RawU.integer

con-integer : {X : ℕ} → ℕ → X ⊢
con-integer n = (con (tmCon integer (Int.pos n)))

_ : ƛ (` zero) · (con-integer {0} 42) ⟶ (con-integer 42)
_ = β con

_ : ƛ (` zero) · (con-integer {0} 42) ⟶* (con-integer 42)
_ = trans (β con) refl

_ : ƛ (` zero) · (con-integer {0} 42) ≅ (con-integer 42)
_ = reduce (trans (β con) refl) refl
```

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

### Enter Nix Shell for a Specific GHC Version

Source: https://github.com/intersectmbo/plutus/blob/master/CONTRIBUTING.adoc

Enter a Nix shell environment with a specific GHC version installed. This is an alternative to using `nix develop` for testing.

```bash
nix develop .#ghc<version>
```

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

### Valid Job ID Examples

Source: https://github.com/intersectmbo/plutus/blob/master/plutus-benchmark/uplc-evaluator/SPEC.md

Provides examples of valid UUID v4 formatted job identifiers that should be used for submissions. These adhere to the RFC 4122 standard.

```text
550e8400-e29b-41d4-a716-446655440000
```

```text
a1b2c3d4-e5f6-4789-a012-3456789abcde
```

```text
f7e8d9c0-b1a2-4567-8901-234567890abc
```

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

### Basic SSH Connection

Source: https://github.com/intersectmbo/plutus/blob/master/plutus-benchmark/uplc-evaluator/SPEC.md

Connect to the benchmarking server using SSH with a specified private key.

```bash
ssh -i ~/.ssh/id_ed25519_plutus benchmarking@benchmarking.plutus.internal
```

```bash
# Connection with custom port (if non-standard port is used)
ssh -i ~/.ssh/id_ed25519_plutus -p 2222 benchmarking@benchmarking.plutus.internal
```

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

### FoldArgs Example

Source: https://github.com/intersectmbo/plutus/blob/master/plutus-core/docs/BuiltinsOverview.md

Illustrates how `FoldArgs` reconstructs a function type by folding a list of argument types with the function constructor `(->)`. This specific example shows `() -> Bool -> Integer`.

```haskell
FoldArgs [(), Bool] Integer
```

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

### Pseudocode Transaction Output Example

Source: https://github.com/intersectmbo/plutus/blob/master/doc/notes/extended-utxo/ValidatingTheNextDataScript.md

This pseudocode demonstrates how to populate a transaction output list with heterogeneous values using the `cast` builtin. Each entry contains a hash and a function that can cast a value to a specific type `b`.

```plutus
txOutput :
    list (hash × (all b. maybe b))
txOutput =
    [ ("aaa", /\b -> cast {integer 1}    {b} (1!1)  ) 
    , ("bbb", /\b -> cast {unit}         {b} unitval)
    , ("ccc", /\b -> cast {bool -> bool} {b} not    )
    ]
```

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

### Example Terms for FloatOut

Source: https://github.com/intersectmbo/plutus/blob/master/plutus-metatheory/src/VerifiedCompilation/FloatOut.lagda.md

Defines basic terms `c` (a constructor) and `id` (the identity function) used in subsequent examples to test the FloatOut relation and its decision procedure.

```lagda
private module Examples where
  open import Relation.Binary.PropositionalEquality
  open import Data.Bool
  open import Data.List using ([])
  open import Data.Fin

  c : ∀ {X} → X ⊢
  c = constr 0 []

  id : ∀ {X} → X ⊢
  id = ƛ (` zero)
```

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

### Upload Program and Configuration Files via SCP

Source: https://github.com/intersectmbo/plutus/blob/master/plutus-benchmark/uplc-evaluator/SPEC.md

Uploads UPLC program and optional configuration files to the benchmarking input directory using SCP.

```bash
# Upload program file
scp program.uplc.txt plutus-benchmarking:/benchmarking/input/${JOB_ID}.uplc.txt
```

```bash
# Upload configuration (optional)
scp config.json plutus-benchmarking:/benchmarking/input/${JOB_ID}.config.json
```

```bash
# Alternative: Upload flat-encoded program
scp program.uplc.flat plutus-benchmarking:/benchmarking/input/${JOB_ID}.uplc.flat
```

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

### Plutus CLI Usage Help

Source: https://github.com/intersectmbo/plutus/blob/master/doc/docusaurus/docs/using-plinth/cli-plutus.md

Consult the Plutus CLI tool's general usage instructions.

```shell
USAGE: plutus [--run|--debug] [-OLEVEL] FILES... [-o FILE]
```

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

### Example of Immediate Unlifting Failure

Source: https://github.com/intersectmbo/plutus/blob/master/doc/adr/adr4.md

This example demonstrates how an immediate unlifting failure occurs when a non-integer string is applied to the addInteger builtin, even before the builtin is fully applied.

```plutus-core
[(builtin addInteger) (con string "hello")]
```

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

### Create Custom UPLC Configuration

Source: https://github.com/intersectmbo/plutus/blob/master/plutus-benchmark/uplc-evaluator/SPEC.md

Creates an example JSON configuration file for UPLC evaluation, specifying protocol version, ledger language, and UPLC version.

```json
# Example configuration for protocol v10, PlutusV3
cat > config.json <<'EOF'
{
  "protocol_version": 10,
  "ledger_language": "PlutusV3",
  "uplc_version": "1.1.0",
  "cost_model_params": null
}
EOF
```

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

### Example: Nested force and delay with error

Source: https://github.com/intersectmbo/plutus/blob/master/plutus-metatheory/src/VerifiedCompilation/UForceDelay.lagda.md

Shows the translation of nested `force` and `delay` operators applied to an `error` term. This example utilizes `translationfd` with `TransMatch.force`, `forcedelay`, and `TransMatch.error`.

```Agda
_ : pureFD {1} (force (force (delay (delay error)))) error
_ = translationfd (Translation.match (TransMatch.force (Translation.istranslation (forcedelay (translationfd reflexive))))) ⨾ forcedelay (translationfd (Translation.match TransMatch.error))
```

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

### Example Configuration: Historical Protocol Version

Source: https://github.com/intersectmbo/plutus/blob/master/plutus-benchmark/uplc-evaluator/SPEC.md

This configuration simulates the Vasil hard fork environment, using Protocol version 7 and PlutusV2 ledger language with UPLC version 1.0.0.

```json
{
  "protocol_version": 7,
  "ledger_language": "PlutusV2",
  "uplc_version": "1.0.0",
  "cost_model_params": null
}
```

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

### Extremely Large Type t_7 Example

Source: https://github.com/intersectmbo/plutus/blob/master/doc/notes/fomega/expensive-types/writeup.md

Presents a fully expanded example of the type t_7, demonstrating its immense size and complexity, which leads to a very high number of reduction steps.

```plutus-core
(\(f::(((((((* -> *) -> (* -> *)) -> ((* -> *) -> (* -> *))) - 
> (((* -> *) -> (* -> *)) -> ((* -> *) -> (* -> *)))) -> ((((* 
-> *) -> (* -> *)) -> ((* -> *) -> (* -> *))) -> (((* -> *) -> (* -> *)) -> ((* -> *) -> (* -> *)))))) -> (((((* -> *) -> (* -> *)) -> ((* -> *) -> (* -> *))) -> (((* -> *) -> (* -> *)) -> ((* -> *) -> (* -> *))))) -> (((((* -> *) -> (* -> *)) -> ((* -> *) -> (* -> *))) -> (((* -> *) -> (* -> *)) -> ((* -> *) -> (* -> *))))))) -> ((((((* -> *) -> (* -> *)) -> ((* -> *) -> (* -> *))) -> (((* -> *) -> (* -> *)) -> ((* -> *) -> (* -> *)))) -> (((((* -> *) -> (* -> *)) -> ((* -> *) -> (* -> *))) -> (((* -> *) -> (* -> *)) -> ((* -> *) -> (* -> *))))) -> (((((* -> *) -> (* -> *)) -> ((* -> *) -> (* -> *))) -> (((* -> *) -> (* -> *)) -> ((* -> *) -> (* -> *)))))))).\(x::((((((* -> *) -> (* -> *)) -> ((* -> *) -> (* -> *))) -> (((* -> *) -> (* -> *)) -> ((* -> *) -> (* -> *)))) -> ((((* -> *) -> (* -> *)) -> ((* -> *) -> (* -> *))) -> (((* -> *) -> (* -> *)) -> ((* -> *) -> (* -> *))))) -> (((((* -> *) -> (* -> *)) -> ((* -> *) -> (* -> *))) -> (((* -> *) -> (* -> *)) -> ((* -> *) -> (* -> *)))) -> ((((* -> *) -> (* -> *)) -> ((* -> *) -> (* -> *))) -> (((* -> *) -> (* -> *)) -> ((* -> *) -> (* -> *))))))). f(f x)) (\(f::((((((* -> *) -> (* -> *)) -> ((* -> *) -> (* -> *))) -> (((* -> *) -> (* -> *)) -> ((* -> *) -> (* -> *)))) -> ((((* -> *) -> (* -> *)) -> ((* -> *) -> (* -> *))) -> (((* -> *) -> (* -> *)) -> ((* -> *) -> (* -> *))))) -> (((((* -> *) -> (* -> *)) -> ((* -> *) -> (* -> *))) -> (((* -> *) -> (* -> *)) -> ((* -> *) -> (* -> *)))) -> ((((* -> *) -> (* -> *)) -> ((* -> *) -> (* -> *))) -> (((* -> *) -> (* -> *)) -> ((* -> *) -> (* -> *))))))).\(x::(((((* -> *) -> (* -> *)) -> ((* -> *) -> (* -> *))) -> (((* -> *) -> (* -> *)) -> ((* -> *) -> (* -> *)))) -> ((((* -> *) -> (* -> *)) -> ((* -> *) -> (* -> *))) -> (((* -> *) -> (* -> *)) -> ((* -> *) -> (* -> *)))))). f(f x)) (\(f::(((((* -> *) -> (* -> *)) -> ((* -> *) -> (* -> *))) -> (((* -> *) -> (* -> *)) -> ((* -> *) -> (* -> *)))) -> ((((* -> *) -> (* -> *)) -> ((* -> *) -> (* -> *))) -> (((* -> *) -> (* -> *)) -> ((* -> *) -> (* -> *)))))). \(x::((((* -> *) -> (* -> *)) -> ((* -> *) -> (* -> *))) -> (((* -> *) -> (* -> *)) -> ((* -> *) -> (* -> *))))). f(f x)) (\(f::((((* -> *) -> (* -> *)) -> ((* -> *) -> (* -> *))) -> (((* -> *) -> (* -> *)) -> ((* -> *) -> (* -> *))))). \(x::(((* -> *) -> (* -> *)) -> ((* -> *) -> (* -> *)))). f(f x)) (\(f::(((* -> *) -> (* -> *)) -> ((* -> *) -> (* -> *)))). \(x::((* -> *) -> (* -> *))). f (f x)) (\(f::((* -> *) -> (* -> *))). \(x::(* -> *)). f (f x)) (\(f::(* -> *)). \(x::*). f (f x))
```

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

### Build Agda documentation

Source: https://github.com/intersectmbo/plutus/blob/master/plutus-metatheory/README.md

Generate static HTML documentation from Agda literate files. This command uses `agda-with-stdlib` for processing and `jekyll` for building the site.

```bash
$ agda-with-stdlib --html --html-highlight=auto --html-dir=html src/index.lagda.md
$ jekyll build -s html -d html/_site
```

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

### Haskell Kind Signature: Bad Example

Source: https://github.com/intersectmbo/plutus/blob/master/STYLEGUIDE.adoc

Example of a data type definition missing a kind signature. Kind signatures are required for type definitions with parameters not all of kind 'Type'.

```Haskell
data Term tyname name uni fun a

```

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

### Type-level RenderConfig Example

Source: https://github.com/intersectmbo/plutus/blob/master/plutus-core/docs/Pretty-printing.md

Illustrates a type signature using a type-level RenderConfig for pretty-printing. This approach aims to integrate configuration directly into the type system.

```Haskell
f :: Term ('RenderConfig 'Debug 'Formatted 'Annotated) -> ...
```

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

### Install Pre-commit Hook

Source: https://github.com/intersectmbo/plutus/blob/master/CONTRIBUTING.adoc

If you encounter 'pre-commit not found' when committing outside of 'nix develop', you can install pre-commit using pip. Alternatively, use the '--no-verify' flag with 'git commit'.

```bash
pip install pre-commit
```

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

### Plutus Core Non-Inferrable Term Example

Source: https://github.com/intersectmbo/plutus/blob/master/doc/notes/fomega/deep-isorecursive/problem.md

Presents a term that type checks but cannot be uniquely inferred due to its structure. This example demonstrates the limitations of the current type inference rules for 'wrap'.

```plutus-core
wrap (r :: * -> *) \(any :: *) -> boolean) true

```

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

### List Available Benchmarks with Cabal

Source: https://github.com/intersectmbo/plutus/blob/master/plutus-benchmark/nofib/README.md

Use this command to list all available nofib benchmarks when using `cabal` for building.

```bash
cabal bench plutus-benchmark:nofib --benchmark-options --list
```

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

### Plutus IR Example: Constructing List [1]

Source: https://github.com/intersectmbo/plutus/blob/master/doc/notes/plutus-ir/plutus-ir.md

Illustrates the construction of a list containing the integer 1 using Plutus IR syntax. It demonstrates let-bindings for recursive datatypes and type aliases.

```haskell
# bind List
(let (rec)
    (datatypebind
        (datatype
            (tyvardecl List (fun (type) (type)))
            (tyvardecl a (type))
            match_List
            (vardecl
                Nil
                [List a]
            )
            (vardecl
                Cons
                (fun a [List a])
            )
        )
    )
    # bind int64 for convenience
    (typebind (tyvardecl int (type)) [(con integer) (con 64)])
    # apply cons to 1 and nil
    [ { Cons int } (con 64 ! 1) { Nil int } ]
)
```

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

### Haskell User Computation Example

Source: https://github.com/intersectmbo/plutus/blob/master/doc/adr/adr2.md

An example of a user computation that interacts with the machine by receiving commands, logging messages, and stepping through the CEK state. This demonstrates the recursive nature of user computations.

```haskell
userComputation :: CekState -> FreeT RequestF SteppableCekM ()
    userComputation currentState = do
      cmd <- inputF
      case cmd of
        Step -> do
          logF "Received Step command"
          mState <- stepF currentState
          userComputation mState
        ...
```

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

### Zerocoupon CEK Node Type Counts

Source: https://github.com/intersectmbo/plutus/blob/master/doc/notes/plutus-core/cek-budgeting-profiling/CekProfiling.md

Statistics on the number of calls to different PLC node types within the Zerocoupon example during CEK evaluation. Provides insight into the computational patterns of this specific example.

```text
   70,640 calls to compute_cek
   45,607 calls to return_cek

   Var:     20,419
   Lam:     19,056
   Apply:   19,353
   Const:   283
   Delay:   4,217
   Force  : 6,900
   Builtin: 412
   Error  : 0
```

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

### Builtin Signature Ambiguity Example

Source: https://github.com/intersectmbo/plutus/blob/master/doc/notes/fomega/evaluation/builtin-evaluation.md

Demonstrates how different builtins with seemingly identical type signatures can have distinct behaviors regarding partial application and computation.

```plutus-core
b₁ with the signature `[](int, int)int`
```

```plutus-core
b₂ with the signature `[](int)(int → int)`
```

```plutus-core
[(builtin b₁) (con 1)]
```

```plutus-core
[(builtin b₂) (con 1)]
```

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

### Enable Profiling in Nix Shell

Source: https://github.com/intersectmbo/plutus/blob/master/CONTRIBUTING.adoc

Enter a Nix shell with all dependencies pre-built with profiling enabled. This process is not cached and can take a long time.

```bash
nix develop .#profiled
```