Skip to content

Instantly share code, notes, and snippets.

@rntz
rntz / MinimalNBE.hs
Last active May 13, 2024 09:17
Normalisation by evaluation for the simply-typed lambda calculus, in Agda
-- A simply-typed lambda calculus, and a definition of normalisation by
-- evaluation for it.
--
-- The NBE implementation is based on a presentation by Sam Lindley from 2016:
-- http://homepages.inf.ed.ac.uk/slindley/nbe/nbe-cambridge2016.pdf
--
-- Adapted to handle terms with explicitly typed contexts (Sam's slides only
-- consider open terms with the environments left implicit/untyped). This was a
-- pain in the ass to figure out.
# This file was auto-generated by cabal2nix. Please do NOT edit manually!
{ cabal, convertible, exceptions, HDBC, HDBCSqlite3, monadHdbc, mtl
, options, text, time, transformers
}:
cabal.mkDerivation (self: {
pname = "scrumgr";
version = "0.1.0.0";
src = ./.;