Index of /~nad/listings/simply-typed

	Name	Last modified	Size	Description
	Parent Directory		-
	Agda.Builtin.Bool.html	2016-12-08 10:59	4.6K
	Agda.Builtin.Equalit..>	2016-12-08 10:59	4.6K
	Agda.Builtin.Nat.html	2016-12-08 10:59	31K
	Agda.Builtin.TrustMe..>	2016-12-08 10:59	3.3K
	Agda.Builtin.Unit.html	2016-12-08 10:59	2.5K
	Agda.Primitive.html	2016-12-08 10:59	6.7K
	Agda.css	2016-12-08 10:59	1.2K
	Data.Bool.Base.html	2016-12-08 10:59	21K
	Data.Empty.html	2016-12-08 10:59	4.2K
	Data.Maybe.Base.html	2016-12-08 10:59	58K
	Data.Nat.Base.html	2016-12-08 10:59	102K
	Data.Nat.html	2016-12-08 10:59	35K
	Data.Product.html	2016-12-08 10:59	95K
	Data.Star.Properties..>	2016-12-08 10:59	100K
	Data.Star.html	2016-12-08 10:59	99K
	Data.Sum.html	2016-12-08 10:59	39K
	Data.Unit.Base.html	2016-12-08 10:59	3.6K
	Data.Unit.NonEta.html	2016-12-08 10:59	12K
	Data.Unit.html	2016-12-08 10:59	20K
	Function.Equality.html	2016-12-08 10:59	67K
	Function.Equivalence..>	2016-12-08 10:59	66K
	Function.Injection.html	2016-12-08 10:59	30K
	Function.html	2016-12-08 10:59	71K
	HOAS.SimplyTyped.Eva..>	2016-12-08 10:59	13K
	HOAS.SimplyTyped.Nor..>	2016-12-08 10:59	25K
	HOAS.SimplyTyped.Nor..>	2016-12-08 10:59	4.3K
	HOAS.SimplyTyped.Typ..>	2016-12-08 10:59	13K
	HOAS.SimplyTyped.Val..>	2016-12-08 10:59	32K
	HOAS.SimplyTyped.html	2016-12-08 10:59	47K
	Level.html	2016-12-08 10:59	5.6K
	Relation.Binary.Cons..>	2016-12-08 10:59	11K
	Relation.Binary.Cons..>	2016-12-08 10:59	119K
	Relation.Binary.Core..>	2016-12-08 10:59	124K
	Relation.Binary.Hete..>	2016-12-08 10:59	9.8K
	Relation.Binary.Inde..>	2016-12-08 10:59	40K
	Relation.Binary.Inde..>	2016-12-08 10:59	16K
	Relation.Binary.Part..>	2016-12-08 10:59	4.6K
	Relation.Binary.Preo..>	2016-12-08 10:59	24K
	Relation.Binary.Prop..>	2016-12-08 10:59	17K
	Relation.Binary.Prop..>	2016-12-08 10:59	8.9K
	Relation.Binary.Prop..>	2016-12-08 10:59	141K
	Relation.Binary.html	2016-12-08 10:59	164K
	Relation.Nullary.Dec..>	2016-12-08 10:59	68K
	Relation.Nullary.html	2016-12-08 10:59	7.5K
	SimplyTyped.Applicat..>	2016-12-08 10:59	15K
	SimplyTyped.ContextE..>	2016-12-08 10:59	11K
	SimplyTyped.Environm..>	2016-12-08 10:59	10K
	SimplyTyped.Evaluati..>	2016-12-08 10:59	19K
	SimplyTyped.NormalFo..>	2016-12-08 10:59	31K
	SimplyTyped.Normalis..>	2016-12-08 10:59	5.8K
	SimplyTyped.Semantic..>	2016-12-08 10:59	35K
	SimplyTyped.Semantic..>	2016-12-08 10:59	41K
	SimplyTyped.Substitu..>	2016-12-08 10:59	71K
	SimplyTyped.TypeSyst..>	2016-12-08 10:59	19K
	SimplyTyped.Value.html	2016-12-08 10:59	55K

------------------------------------------------------------------------
-- Normalisation for the simply typed λ-calculus
------------------------------------------------------------------------

module README where

------------------------------------------------------------------------
-- Using de Bruijn indices

-- The type system.

import SimplyTyped.TypeSystem

-- Applicative structures.

import SimplyTyped.ApplicativeStructure

-- Environments.

import SimplyTyped.Environment

-- Evaluating terms.

import SimplyTyped.Evaluation

-- Context extensions.

import SimplyTyped.ContextExtension

-- Substitutions.

import SimplyTyped.Substitution

-- Normal forms.

import SimplyTyped.NormalForm

-- Values.

import SimplyTyped.Value

-- Normalisation.

import SimplyTyped.Normalisation

-- Semantics (not used for anything).

import SimplyTyped.Semantics
import SimplyTyped.Semantics.Lemmas

------------------------------------------------------------------------
-- Using PHOAS

-- The following modules mirror most of the development above, but use
-- HOAS (more specifically, Adam Chlipala's PHOAS) instead of
-- de Bruijn indices.

import HOAS.SimplyTyped.TypeSystem
import HOAS.SimplyTyped.Evaluation
import HOAS.SimplyTyped.NormalForm
import HOAS.SimplyTyped.Value
import HOAS.SimplyTyped.Normalisation

-- A condensed version of the HOAS.SimplyTyped modules above (no
-- comments, but no imports and less than one page long).

import HOAS.SimplyTyped