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

