Skip to content

Instantly share code, notes, and snippets.

roconnor

Block or report user

Report or block roconnor

Hide content and notifications from this user.

Learn more about blocking users

Contact Support about this user’s behavior.

Learn more about reporting abuse

Report abuse
View GitHub Profile
@rntz
rntz / MinimalNBE.hs
Last active Apr 21, 2019
Normalisation by evaluation for the simply-typed lambda calculus, in Agda
View MinimalNBE.hs
-- 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.
View default.nix
# 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 = ./.;
You can’t perform that action at this time.