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.

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

Walkthrough groups

• Proofs - Kernel-checked proof walkthroughs: computation, equality reasoning, and verified extraction.
• Effects and Validation - Effect-handler walkthroughs that show one computation running under multiple validation policies.
• Surface Languages - Small source-language walkthroughs built over HOAS, refinements, diagnostics, and generated data.
• Applications - Complete example programs that double as benchmark workloads.