- arith

   simple arithmetic functions
   * arith.bel

- copy

  copying recursively lambda-terms
   * copy-simple.bel            (simply typed)
   * copy-simple-explicit.bel   (simply typed, fully explicit)
   * copy.bel                   (dependently typed)
   * copy-explicit.bel          (dependently typed, fully explicit)


   Copying recursively lambda-terms.

- count-var

  Variable counting example containing typed expressions z, suc, tt, add
  and letv.

  This example illustrates that reconstructing all implicit type
  arguments in patterns is slightly limitting, since we may learn
  further information about some of them in the actual branch.

  * cntvar.bel
  * cntvar-explicit.bel (fully explicit version)
  * cntvar-2.bel  (same as cntvar.bel with different plus function)

- free-vars

  Checks if a typed expression contains a free variable.
  * fvnat.bel
  * fvnat-explicit.bel

- LF
   Contains several pure LF examples.


- lp-horn

   Contains encoding of natural deduction, together with canonical proofs, and uniform proofs.
   These are adapted from the Twelf repository. The proofs cannot be implemented in Beluga yet,
   since they require context coercions.

- mini-ml

  * * eval-sub.bel
    * eval-sub-explicit.bel

     Substitution-based interpreter for a simple
     functional language containing z, suc, letn, letv,
     app, lam and fix.

    * eval-sub-1.bel
    * eval-sub-1-explicit

      Substitution-based interpreter for simple language
      containing natural numbers, add, and let-expresion.
      (see POPL'08)

    * tps.bel
       Type preservation proof implemented as Beluga program
       for z, s, match, letv, lam, app

    * vsound.bel
    * vsound-explicit.bel
       Value soundness proof implemented as Beluga program
       for z, s, letv. lam, app


- small-step

   Small-step step semantics for Church-style simply-typed lambda-calculus
   including preservation and progress proof.
   The function prog' implements progress by exploiting inversion properties.

   NOTE: function prog is incomplete -- in fact, it is impossible to write
   this function currently in Beluga.

- test

  Contains various simple test files for different features


- typed-eval

   Contains a substitution-based interpreter which only evaluates well-typed expressions
   It includes tt, ff, z, suc, iff, eq, letv

- polylam

  * normal.bel

    converts an expression in a simply typed lambda calculus to a
    normal form (changing the representation to a value only representation)

Notworking
------------------

- tpcert.bel
   Not working because Sigma-types are not handled


- cut-elim.bel
    Twelf Proof is not converted into functional program
    may also require sigma-types?

- eq-proof.bel
    Should be converted to new syntax; seems to require sigma-types
    NOTE: current definition of schema W is WRONG. It should be

     schema W = some [] block {x:exp}eq x x;

- tpeval.bel

    No handling of substitution variables yet.


- fol-handbool.bel

    Needs context coercions, and sigma-types in context schemas


- debruijn

    Example taken from Twelf examples/compile.
    It needs Sigma-types in computations to state the main theorem:

    rec map_eval: (eval E V)[ ] -> (trans K F E)[ ]
      -> Sigma W. (feval K F W)[ ] *  (vtrans W V)[ ] =

    In addition, we need to be able to compare two LF objects for equality
    and propagate type information. If [ ] D' : eval E E = [ ] D : eval E V
    then   E = V.


- debruijn1

    Example taken from Twelf examples/compile.
    It needs Sigma-types in computations.

     rec map_eval : (eval E V)[ ] -> (trans K F E)[ ]
 	        -> Sigma W . (feval K F W)[ ] * (vtrans W V)[ ] =
