From: acondolu <andrea.condoluci@unibo.it>
Date: Mon, 28 May 2018 15:08:46 +0000 (+0200)
Subject: Tentative implementation of strong separation algorithm
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5a57b32e5e068d05c1feb7455861bc8d5e4bd05a;hp=5a57b32e5e068d05c1feb7455861bc8d5e4bd05a;p=fireball-separation.git

Tentative implementation of strong separation algorithm

- A `Match from num is translated to pure by masking branches
  with underscore lambdas
- The eating step on the divergent does not create a substitution in sigma
  (to be understood...)
- In the branch of matches, \_. !divergent is translated to delta
- The checks in dangerous must still be fixed to go under lambdas
---