GitLab

The printer exists but is not yet usable.

- move compile_match to Eliminate_algebraic
- move eliminate_builtin to Eliminate_definition

Pour que l'on donne toujours les mêmes déclarations pour le type à encoder dans plusieurs taches différentes

- use simplifying constructors in "eliminate_definition"

I will always compile before committing
I will always compile before committing
I will...

like f_map_sign should only be applied from specialized
recursive functions and these funcitons will usually supply
the polarity argument.

In particular, it is now independent of compile_match.

of eliminate_ite, based on continuation-passing map.

François, I don't really intend to redo everything you do, honest!
It's just that I reflected on this solution since Friday and was
too enthralled with it to abandon it.