![[ICO]](/icons/blank.gif){kind=icon}
![[DIR]](/icons/back.gif){kind=icon}
![[TXT]](/icons/text.gif){kind=icon}
| Name | Last modified | Size | Description |
|---|---|---|---|---|
| Parent Directory | - | ||
| Agda.css | 26-Oct-2010 14:02 | 1.1K | |
| Data.Empty.html | 26-Oct-2010 14:02 | 3.8K | |
| Data.Maybe.Core.html | 26-Oct-2010 14:02 | 4.6K | |
| Data.Nat.html | 26-Oct-2010 14:02 | 124K | |
| Data.Product.html | 26-Oct-2010 14:02 | 91K | |
| Data.Star.Properties..> | 26-Oct-2010 14:02 | 93K | |
| Data.Star.html | 26-Oct-2010 14:02 | 80K | |
| Data.Sum.html | 26-Oct-2010 14:02 | 36K | |
| Function.Equality.html | 26-Oct-2010 14:02 | 62K | |
| Function.Injection.html | 26-Oct-2010 14:02 | 27K | |
| Function.html | 26-Oct-2010 14:02 | 53K | |
| HOAS.SimplyTyped.Eva..> | 26-Oct-2010 14:02 | 14K | |
| HOAS.SimplyTyped.Nor..> | 26-Oct-2010 14:02 | 25K | |
| HOAS.SimplyTyped.Nor..> | 26-Oct-2010 14:02 | 5.3K | |
| HOAS.SimplyTyped.Typ..> | 26-Oct-2010 14:02 | 12K | |
| HOAS.SimplyTyped.Val..> | 26-Oct-2010 14:02 | 32K | |
| HOAS.SimplyTyped.html | 26-Oct-2010 14:02 | 47K | |
| Level.html | 26-Oct-2010 14:02 | 10K | |
| README.html | 26-Oct-2010 14:02 | 10K | |
| Relation.Binary.Cons..> | 26-Oct-2010 14:02 | 11K | |
| Relation.Binary.Cons..> | 26-Oct-2010 14:02 | 89K | |
| Relation.Binary.Core..> | 26-Oct-2010 14:02 | 132K | |
| Relation.Binary.EqRe..> | 26-Oct-2010 14:02 | 7.2K | |
| Relation.Binary.Inde..> | 26-Oct-2010 14:02 | 42K | |
| Relation.Binary.Inde..> | 26-Oct-2010 14:02 | 17K | |
| Relation.Binary.Part..> | 26-Oct-2010 14:02 | 5.3K | |
| Relation.Binary.Preo..> | 26-Oct-2010 14:02 | 21K | |
| Relation.Binary.Prop..> | 26-Oct-2010 14:02 | 18K | |
| Relation.Binary.Prop..> | 26-Oct-2010 14:02 | 83K | |
| Relation.Binary.html | 26-Oct-2010 14:02 | 140K | |
| Relation.Nullary.Cor..> | 26-Oct-2010 14:02 | 7.9K | |
| Relation.Nullary.html | 26-Oct-2010 14:02 | 3.8K | |
| SimplyTyped.Applicat..> | 26-Oct-2010 14:02 | 15K | |
| SimplyTyped.ContextE..> | 26-Oct-2010 14:02 | 11K | |
| SimplyTyped.Environm..> | 26-Oct-2010 14:02 | 10K | |
| SimplyTyped.Evaluati..> | 26-Oct-2010 14:02 | 20K | |
| SimplyTyped.NormalFo..> | 26-Oct-2010 14:02 | 31K | |
| SimplyTyped.Normalis..> | 26-Oct-2010 14:02 | 6.4K | |
| SimplyTyped.Semantic..> | 26-Oct-2010 14:02 | 35K | |
| SimplyTyped.Semantic..> | 26-Oct-2010 14:02 | 41K | |
| SimplyTyped.Substitu..> | 26-Oct-2010 14:02 | 70K | |
| SimplyTyped.TypeSyst..> | 26-Oct-2010 14:02 | 18K | |
| SimplyTyped.Value.html | 26-Oct-2010 14:02 | 56K | |
------------------------------------------------------------------------ -- 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