GitHub - ashley-woodard/nano-Agda: Tiny type-checker with dependent types

Branches Tags

Name		Name	Last commit message	Last commit date
Latest commit History 7 Commits
examples		examples
.gitignore		.gitignore
AbsSynToTerm.hs		AbsSynToTerm.hs
Basics.hs		Basics.hs
Display.hs		Display.hs
LICENSE		LICENSE
Main.hs		Main.hs
Normal.hs		Normal.hs
Options.hs		Options.hs
README		README
RawSyntax.hs		RawSyntax.hs
Terms.hs		Terms.hs
TestSyntax.hs		TestSyntax.hs
TypeCheckerNF.hs		TypeCheckerNF.hs
nanoAgda.cabal		nanoAgda.cabal

Repository files navigation

A tiny type-checker, loosely based on 

 "On the Algebraic Foundation of Proof Assistants for Intuitionistic Type Theory", Abel, Coquand, Dybjer.

some ideas from

"A Tutorial Implementation of a Dependently Typed Lambda Calculus", Löh, McBride, Swierstra

are also used for this implementation.

Additionally, this implementation performs evaluation to normal form
and type checking/inference at the same time. Some extra features,
that add a lot of convenience, but just little complication are also
present, such as dependent sums.

The interesting bits are in 

Normal.hs (mainly the subst function which performs hereditary substitutions)
TypeCheckerNF.hs (type checking and driver of normalisation)