Examples
Worked examples for proofs, effect-handler policy, and small surface languages over HOAS.
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.
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.
examples/
proof-basics.nix
equality-proofs.nix
verified-functions.nix
handler-swap-validation.nix
stlc/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.