Normalisation by evaluation 2

[AustenPrinciple]

This time it's sort of put inside the kernel, and validates lein test :all. It's unclear to me as to whether it actually works or not

[fredokun]

Sounds like a very good PR, however I cannot merge it in master, could you use the branch nbe that I've just created... One test you could do is to just check the time for performing the tests, for a start. But we will need to test the new scheme on all Latte libraries. I would prefer to keep the old beta-step so we can make non-regression tests... It means that in norm we should be able (using a global variable let's say) to :

• use only the old beta-step
• use only the new nbe scheme
• use both and compare each time there's a normalization that we obtain alpha-equivalent results

And all this go into a nbe branch (we will use the same branch name in all the other parts of LaTTe).

So for now I close this PR.

[fredokun]

I should add : could you make a PR to master just for the cleanup you've done, and after I merge this into master a specific PR with just the nbe stuff ? (Sorry for the extra work but that will make a better project history)