# Examples


The examples show nix-effects in complete, small programs. They move
from proof construction, to effect-handler policy, to surface languages
built over the HOAS kernel, to application-sized interpreters and graph
evaluators.

The same examples live in the source tree under `examples/` if you want
to run or adapt them locally.

## Where to start

Start with proof examples when you want to see values checked by the
kernel. Use the effect example to compare validation policies without
changing the computation. Use the surface-language examples when you
want to build a small syntax layer over HOAS. Use the application
examples when you want complete programs that also feed the benchmark
suite.

```nix
examples/
  proof-basics.nix
  equality-proofs.nix
  verified-functions.nix
  handler-swap-validation.nix
  stlc/
  category-theory/
  interp/
  build-sim/
```

## Walkthrough groups

- [Proofs](/nix-effects/proof-examples) - Kernel-checked proof walkthroughs: computation, equality reasoning, and verified extraction.
- [Effects and Validation](/nix-effects/effect-examples) - Effect-handler walkthroughs that show one computation running under multiple validation policies.
- [Surface Languages](/nix-effects/surface-examples) - Small source-language walkthroughs built over HOAS, refinements, diagnostics, and generated data.
- [Applications](/nix-effects/application-examples) - Complete example programs that double as benchmark workloads.