Index of /~nad/listings/simply-typed

[ICO]NameLast modifiedSizeDescription

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

README
------------------------------------------------------------------------
-- 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