Surface STLC
The STLC examples build a source language incrementally over the HOAS
checker. Each child page introduces one extension, with the full source
available under examples/stlc/.
Layered surfaces
The core surface defines functions and application. Later examples import that vocabulary and extend it with products, sums, recursive lists, refinements, and diagnostics.
core = import ./core.nix { inherit fx lib; };
sumsProducts = import ./sums-products.nix { inherit fx lib core; };
recursiveLists = import ./recursive-lists.nix { inherit fx lib core; };
refinementsDiagnostics = import ./refinements-diagnostics.nix {
inherit fx lib core;
};