…me reason."

This reverts commit 7e32f742fa318b19e41ab7d99d39496645304427.

the  folder may have contained useful stuff. Check history if needed.

There's an unrestricted smt left in RP.ec, because of the goal:

d_ll: is_lossless dt
d_fu: support dt = predT
&m: memory <P.f>
h : exists (x : t), ! mem (rng P.m{m}) x
------------------------------------------------------------------------
mu dt (mem (rng P.m{m})) < 1%r

After a quick look, I'm not seeing what combination of distribution
lemmas says that if the support of a distribution d is all of a type t
and some element of t doesn't satisfy a predicate P, that mu d P
< 1.

Maybe the following lemma would be useful addition to EC Library,
as it works well with dexcepted_ll?

lemma mu_except ['a] (d : 'a distr, y : 'a, P : 'a -> bool) :
  is_lossless d => support d = predT => ! P y => mu d P < 1%r.

(Francois just used this logic in IdealPRP.ec; as he says,
maybe we should be using that instead of RP.ec.)

lemma mu_except ['a] (d : 'a distr, y : 'a, P : 'a -> bool) :
  in_supp y d => ! P y => mu d P < mu d predT.

And simplified use of it.

syntax.

I haven't updated the files in the "core" subdirectory, several of
which are now failing to parse.

New and improved functor system really helped with debugging.

Drop '=' as notation for assignments

Issues remain with Jasmin standard libs

- Rewriting no longer performs head delta before matching
- Rework of number libs and algebraic instances

Can't dive into prefix-based hell right now.

Tracking down an issue with pRHL producing ill-formed formulas

Use standard library find, map on finite maps.