Index of /~nad/listings/dependently-typed-syntax

[ICO]NameLast modifiedSizeDescription

[PARENTDIR]Parent Directory   -  
[TXT]deBruijn.Substitutio..>2023-09-29 17:39 59K 
[TXT]deBruijn.Substitutio..>2023-09-29 17:39 239K 
[TXT]deBruijn.Substitutio..>2023-09-29 17:39 67K 
[TXT]deBruijn.Substitutio..>2023-09-29 17:39 155K 
[TXT]deBruijn.Substitutio..>2023-09-29 17:39 98K 
[TXT]deBruijn.Substitutio..>2023-09-29 17:39 271K 
[TXT]deBruijn.Substitutio..>2023-09-29 17:39 104K 
[TXT]deBruijn.Substitutio..>2023-09-29 17:39 171K 
[TXT]deBruijn.Substitutio..>2023-09-29 17:39 4.6K 
[TXT]deBruijn.Substitutio..>2023-09-29 17:39 169K 
[TXT]deBruijn.Substitutio..>2023-09-29 17:39 182K 
[TXT]deBruijn.Substitutio..>2023-09-29 17:39 23K 
[TXT]deBruijn.Substitutio..>2023-09-29 17:39 243K 
[TXT]deBruijn.Substitutio..>2023-09-29 17:39 148K 
[TXT]deBruijn.Substitutio..>2023-09-29 17:39 61K 
[TXT]deBruijn.Context.html 2023-09-29 17:39 4.2K 
[TXT]deBruijn.Context.Ter..>2023-09-29 17:39 182K 
[TXT]deBruijn.Context.Ext..>2023-09-29 17:39 139K 
[TXT]deBruijn.Context.Ext..>2023-09-29 17:39 138K 
[TXT]deBruijn.Context.Ext..>2023-09-29 17:39 40K 
[TXT]deBruijn.Context.Bas..>2023-09-29 17:39 201K 
[TXT]Relation.Unary.html 2023-09-29 17:39 91K 
[TXT]Relation.Nullary.html 2023-09-29 17:39 6.5K 
[TXT]Relation.Nullary.Ref..>2023-09-29 17:39 34K 
[TXT]Relation.Nullary.Neg..>2023-09-29 17:39 38K 
[TXT]Relation.Nullary.Neg..>2023-09-29 17:39 21K 
[TXT]Relation.Nullary.Dec..>2023-09-29 17:39 32K 
[TXT]Relation.Nullary.Dec..>2023-09-29 17:39 56K 
[TXT]Relation.Binary.html 2023-09-29 17:39 1.9K 
[TXT]Relation.Binary.Stru..>2023-09-29 17:39 62K 
[TXT]Relation.Binary.Reas..>2023-09-29 17:39 7.4K 
[TXT]Relation.Binary.Reas..>2023-09-29 17:39 3.5K 
[TXT]Relation.Binary.Reas..>2023-09-29 17:39 69K 
[TXT]Relation.Binary.Reas..>2023-09-29 17:39 20K 
[TXT]Relation.Binary.Reas..>2023-09-29 17:39 45K 
[TXT]Relation.Binary.Prop..>2023-09-29 17:39 53K 
[TXT]Relation.Binary.Prop..>2023-09-29 17:39 4.1K 
[TXT]Relation.Binary.Prop..>2023-09-29 17:39 104K 
[TXT]Relation.Binary.Prop..>2023-09-29 17:39 45K 
[TXT]Relation.Binary.Prop..>2023-09-29 17:39 5.5K 
[TXT]Relation.Binary.Prop..>2023-09-29 17:39 17K 
[TXT]Relation.Binary.Prop..>2023-09-29 17:39 18K 
[TXT]Relation.Binary.Prop..>2023-09-29 17:39 9.8K 
[TXT]Relation.Binary.Prop..>2023-09-29 17:39 34K 
[TXT]Relation.Binary.Morp..>2023-09-29 17:39 38K 
[TXT]Relation.Binary.Morp..>2023-09-29 17:39 6.3K 
[TXT]Relation.Binary.Latt..>2023-09-29 17:39 1.7K 
[TXT]Relation.Binary.Latt..>2023-09-29 17:39 61K 
[TXT]Relation.Binary.Latt..>2023-09-29 17:39 12K 
[TXT]Relation.Binary.Latt..>2023-09-29 17:39 68K 
[TXT]Relation.Binary.Inde..>2023-09-29 17:39 2.1K 
[TXT]Relation.Binary.Inde..>2023-09-29 17:39 13K 
[TXT]Relation.Binary.Inde..>2023-09-29 17:39 10K 
[TXT]Relation.Binary.Inde..>2023-09-29 17:39 13K 
[TXT]Relation.Binary.Inde..>2023-09-29 17:39 15K 
[TXT]Relation.Binary.Inde..>2023-09-29 17:39 11K 
[TXT]Relation.Binary.Defi..>2023-09-29 17:39 91K 
[TXT]Relation.Binary.Core..>2023-09-29 17:39 19K 
[TXT]Relation.Binary.Cons..>2023-09-29 17:39 69K 
[TXT]Relation.Binary.Cons..>2023-09-29 17:39 77K 
[TXT]Relation.Binary.Cons..>2023-09-29 17:39 72K 
[TXT]Relation.Binary.Cons..>2023-09-29 17:39 101K 
[TXT]Relation.Binary.Bund..>2023-09-29 17:39 66K 
[TXT]Level.html 2023-09-29 17:39 5.6K 
[TXT]Induction.html 2023-09-29 17:39 17K 
[TXT]Induction.WellFounde..>2023-09-29 17:39 87K 
[TXT]Function.html 2023-09-29 17:39 2.0K 
[TXT]Function.Surjection...>2023-09-29 17:39 33K 
[TXT]Function.Structures...>2023-09-29 17:39 43K 
[TXT]Function.Strict.html 2023-09-29 17:39 15K 
[TXT]Function.Metric.Stru..>2023-09-29 17:39 22K 
[TXT]Function.Metric.Nat...>2023-09-29 17:39 1.8K 
[TXT]Function.Metric.Nat...>2023-09-29 17:39 18K 
[TXT]Function.Metric.Nat...>2023-09-29 17:39 17K 
[TXT]Function.Metric.Nat...>2023-09-29 17:39 2.6K 
[TXT]Function.Metric.Nat...>2023-09-29 17:39 28K 
[TXT]Function.Metric.Defi..>2023-09-29 17:39 35K 
[TXT]Function.Metric.Core..>2023-09-29 17:39 2.8K 
[TXT]Function.Metric.Bund..>2023-09-29 17:39 37K 
[TXT]Function.LeftInverse..>2023-09-29 17:39 42K 
[TXT]Function.Inverse.html 2023-09-29 17:39 60K 
[TXT]Function.Injection.html2023-09-29 17:39 23K 
[TXT]Function.Equivalence..>2023-09-29 17:39 40K 
[TXT]Function.Equality.html 2023-09-29 17:39 40K 
[TXT]Function.Definitions..>2023-09-29 17:39 21K 
[TXT]Function.Core.html 2023-09-29 17:39 5.0K 
[TXT]Function.Consequence..>2023-09-29 17:39 34K 
[TXT]Function.Consequence..>2023-09-29 17:39 22K 
[TXT]Function.Bundles.html 2023-09-29 17:39 110K 
[TXT]Function.Bijection.html2023-09-29 17:39 33K 
[TXT]Function.Base.html 2023-09-29 17:39 75K 
[TXT]Effect.Monad.html 2023-09-29 17:39 32K 
[TXT]Effect.Functor.html 2023-09-29 17:39 13K 
[TXT]Effect.Empty.html 2023-09-29 17:39 3.4K 
[TXT]Effect.Choice.html 2023-09-29 17:39 4.4K 
[TXT]Effect.Applicative.html2023-09-29 17:39 36K 
[TXT]Data.Universe.html 2023-09-29 17:39 2.6K 
[TXT]Data.Universe.Indexe..>2023-09-29 17:39 6.2K 
[TXT]Data.Unit.html 2023-09-29 17:39 1.7K 
[TXT]Data.Unit.Properties..>2023-09-29 17:39 16K 
[TXT]Data.Unit.Polymorphi..>2023-09-29 17:39 3.3K 
[TXT]Data.Unit.Base.html 2023-09-29 17:39 1.9K 
[TXT]Data.These.Base.html 2023-09-29 17:39 36K 
[TXT]Data.Sum.Base.html 2023-09-29 17:39 26K 
[TXT]Data.Sign.Base.html 2023-09-29 17:39 8.9K 
[TXT]Data.Product.html 2023-09-29 17:39 9.0K 
[TXT]Data.Product.Base.html 2023-09-29 17:39 87K 
[TXT]Data.Parity.Base.html 2023-09-29 17:39 19K 
[TXT]Data.Nat.html 2023-09-29 17:39 5.7K 
[TXT]Data.Nat.Properties...>2023-09-29 17:39 908K 
[TXT]Data.Nat.Base.html 2023-09-29 17:39 83K 
[TXT]Data.Maybe.html 2023-09-29 17:39 7.5K 
[TXT]Data.Maybe.Relation...>2023-09-29 17:39 31K 
[TXT]Data.Maybe.Relation...>2023-09-29 17:39 54K 
[TXT]Data.Maybe.Effectful..>2023-09-29 17:39 20K 
[TXT]Data.Maybe.Base.html 2023-09-29 17:39 37K 
[TXT]Data.Irrelevant.html 2023-09-29 17:39 12K 
[TXT]Data.Empty.html 2023-09-29 17:39 4.1K 
[TXT]Data.Empty.Irrelevan..>2023-09-29 17:39 2.2K 
[TXT]Data.Bool.Properties..>2023-09-29 17:39 204K 
[TXT]Data.Bool.Base.html 2023-09-29 17:39 13K 
[TXT]Axiom.UniquenessOfId..>2023-09-29 17:39 23K 
[TXT]Axiom.UniquenessOfId..>2023-09-29 17:39 2.6K 
[TXT]Axiom.Extensionality..>2023-09-29 17:39 21K 
[TXT]Algebra.html 2023-09-29 17:39 1.9K 
[TXT]Algebra.Structures.html2023-09-29 17:39 210K 
[TXT]Algebra.Structures.B..>2023-09-29 17:39 64K 
[TXT]Algebra.Properties.S..>2023-09-29 17:39 8.2K 
[TXT]Algebra.Properties.G..>2023-09-29 17:39 52K 
[TXT]Algebra.Properties.C..>2023-09-29 17:39 112K 
[TXT]Algebra.Morphism.html 2023-09-29 17:39 47K 
[TXT]Algebra.Morphism.Str..>2023-09-29 17:39 177K 
[TXT]Algebra.Morphism.Def..>2023-09-29 17:39 11K 
[TXT]Algebra.Lattice.Stru..>2023-09-29 17:39 41K 
[TXT]Algebra.Lattice.Prop..>2023-09-29 17:39 11K 
[TXT]Algebra.Lattice.Prop..>2023-09-29 17:39 42K 
[TXT]Algebra.Lattice.Prop..>2023-09-29 17:39 6.0K 
[TXT]Algebra.Lattice.Prop..>2023-09-29 17:39 293K 
[TXT]Algebra.Lattice.Cons..>2023-09-29 17:39 6.3K 
[TXT]Algebra.Lattice.Cons..>2023-09-29 17:39 18K 
[TXT]Algebra.Lattice.Cons..>2023-09-29 17:39 4.5K 
[TXT]Algebra.Lattice.Bund..>2023-09-29 17:39 51K 
[TXT]Algebra.Lattice.Bund..>2023-09-29 17:39 7.2K 
[TXT]Algebra.Definitions...>2023-09-29 17:39 118K 
[TXT]Algebra.Core.html 2023-09-29 17:39 3.3K 
[TXT]Algebra.Construct.Na..>2023-09-29 17:39 109K 
[TXT]Algebra.Construct.Na..>2023-09-29 17:39 57K 
[TXT]Algebra.Construct.Na..>2023-09-29 17:39 18K 
[TXT]Algebra.Construct.Na..>2023-09-29 17:39 17K 
[TXT]Algebra.Consequences..>2023-09-29 17:39 165K 
[TXT]Algebra.Consequences..>2023-09-29 17:39 39K 
[TXT]Algebra.Consequences..>2023-09-29 17:39 7.1K 
[TXT]Algebra.Bundles.html 2023-09-29 17:39 255K 
[TXT]Algebra.Bundles.Raw...>2023-09-29 17:39 54K 
[TXT]Agda.css 2023-09-29 17:39 1.8K 
[TXT]Agda.Primitive.html 2023-09-29 17:39 5.4K 
[TXT]Agda.Builtin.Unit.html 2023-09-29 17:39 1.7K 
[TXT]Agda.Builtin.Strict...>2023-09-29 17:39 4.8K 
[TXT]Agda.Builtin.Sigma.html2023-09-29 17:39 3.4K 
[TXT]Agda.Builtin.Nat.html 2023-09-29 17:39 23K 
[TXT]Agda.Builtin.Maybe.html2023-09-29 17:39 2.3K 
[TXT]Agda.Builtin.Equalit..>2023-09-29 17:39 2.6K 
[TXT]Agda.Builtin.Equalit..>2023-09-29 17:39 2.3K 
[TXT]Agda.Builtin.Bool.html 2023-09-29 17:39 3.1K 

README
------------------------------------------------------------------------
-- A library for working with dependently typed syntax
-- Nils Anders Danielsson
------------------------------------------------------------------------

-- This library is leaning heavily on two of Conor McBride's papers:
--
-- * Type-Preserving Renaming and Substitution.
--
-- * Outrageous but Meaningful Coincidences: Dependent type-safe
--   syntax and evaluation.

-- This module gives a brief overview of the modules in the library.

module README where

------------------------------------------------------------------------
-- The library

-- Contexts, variables, context morphisms, context extensions, etc.

import deBruijn.Context

-- Parallel substitutions (defined using an inductive family).

import deBruijn.Substitution.Data.Basics

-- A map function for the substitutions.

import deBruijn.Substitution.Data.Map

-- Some simple substitution combinators. (Given a term type which
-- supports weakening and transformation of variables to terms various
-- substitutions are defined and various lemmas proved.)

import deBruijn.Substitution.Data.Simple

-- Given an operation which applies a substitution to a term,
-- satisfying some properties, more operations and lemmas are
-- defined/proved.
--
-- (This module reexports various other modules.)

import deBruijn.Substitution.Data.Application

-- A module which repackages (and reexports) the development under
-- deBruijn.Substitution.Data.

import deBruijn.Substitution.Data

-- Some modules mirroring the development under
-- deBruijn.Substitution.Data, but using substitutions defined as
-- functions rather than data.
--
-- The functional version of substitutions is in some respects easier
-- to work with than the one based on data, but in other respects more
-- awkward. I maintain both developments so that they can be compared.

import deBruijn.Substitution.Function.Basics
import deBruijn.Substitution.Function.Map
import deBruijn.Substitution.Function.Simple

-- The two definitions of substitutions are isomorphic (assuming
-- extensionality).

import deBruijn.Substitution.Isomorphic

------------------------------------------------------------------------
-- An example showing how the library can be used

-- A well-typed representation of a dependently typed language.

import README.DependentlyTyped.Term

-- Normal and neutral terms.

import README.DependentlyTyped.NormalForm

-- Instantiation of deBruijn.Substitution.Data for terms.

import README.DependentlyTyped.Term.Substitution

-- Instantiation of deBruijn.Substitution.Data for normal and neutral
-- terms.

import README.DependentlyTyped.NormalForm.Substitution

-- Normalisation by evaluation.

import README.DependentlyTyped.NBE

-- Various equality checkers (some complete, all sound).

import README.DependentlyTyped.Equality-checker

-- Raw terms.

import README.DependentlyTyped.Raw-term

-- A type-checker (sound).

import README.DependentlyTyped.Type-checker

-- A definability result: A "closed value" is the semantics of a
-- closed term if and only if it satisfies all "Kripke predicates".

import README.DependentlyTyped.Definability

-- An observation: There is a term without a corresponding syntactic
-- type (given some assumptions).

import README.DependentlyTyped.Term-without-type

-- Another observation: If the "Outrageous but Meaningful
-- Coincidences" approach is used to formalise a language, then you
-- can end up with an extensional type theory (with equality
-- reflection).

import README.DependentlyTyped.Extensional-type-theory

-- Inductively defined beta-eta-equality.

import README.DependentlyTyped.Beta-Eta

-- TODO: Add an untyped example.