Version 3.2

`bindlib `is a library and a camlp4 extension for the Objective-Caml language providing reasonable tools to write programs
manipulating data structures with bound variables (like lambda-calculus or
quantified formulae). It is quite efficient and easy to
use (thanks to the camlp4 extension).

- Documentation (pdf file, Objective-Caml syntax).
- The Objective-Caml version (version 26/04/2013).
- You can access the current development version via darcs with
`darcs get http://www.lama.univ-savoie.fr/~raffalli/repos/bindlib`

`Bindlib also has a wiki`

```
```## Example

The library comes with some examples, here is one of them: the
normalisation of lambda-terms:
(* lets open the library ! *)
open Bindlib
(* type of pure lambda-terms *)
type term =
App of term * term
| Abs of (term,term) binder
| FVar of term variable
(* weak head normal form *)
let rec whnf = function
App(t1,t2) as t0 -> (
match (whnf t1) with
Abs f -> whnf (subst f t2)
| t1' -> if t1' != t1 then App(t1', t2) else t0)
| t -> t
(* call by name normalisation *)
let norm t = let rec fn t =
match whnf t with
Abs f ->
(match f with bind fVar x in u ->
Abs(^ bindvar x in fn u ^) )
| t ->
let rec unwind = function
FVar(x) -> bindbox_of x
| App(t1,t2) -> App(^unwind t1,fn t2^)
| t -> assert false
in unwind t
in unbox (fn t)

Christophe
Raffalli /LAMA, Savoie University / raffalli@univ-savoie.fr