[ new ] OK by Construction Proof Search for IMLL

This is the way I was describing this work a few weeks ago in
Edinburgh: Resource aware contexts and proof search for IMLL

Starting from the observation that naïve proof search for IMLL is
intractable, we will see how building a notion of resource availability
into the context and massaging the sequent calculus intoa more general
one handling both resource consumption and a notion of "leftovers" of a
subproof allows for a well-structured, well-typed by construction proof
search mechanism.
The fragment we will discuss will consist of `tensor` and `with`.
[ new ] Non Regular Parameters are OK

Nice trick taken from Bruno Barras' habilitation thesis: one can
recover large non regular parameters by using one large parameter
and a small index recording the various deterministic changes
which should be applied to this parameter before it being used.

The example is a small lambda calculus with lambda abstractions as
well as let bindings. A story about containers extended with non-
regular parameters should be told.
[ new ] Dimension-aware computations

This is the code corresponding to my blog post about dimensional
analysis as a type-level computation [1].

/!\ This Agda program is meant to be compiled and will produce an
output if run! :-o

[1] http://blog.gallais.org/read/dimension-aware-computations