]> matita.cs.unibo.it Git - fireball-separation.git/commitdiff
Tentative implementation of strong separation algorithm
authoracondolu <andrea.condoluci@unibo.it>
Mon, 28 May 2018 15:08:46 +0000 (17:08 +0200)
committeracondolu <andrea.condoluci@unibo.it>
Mon, 28 May 2018 15:08:46 +0000 (17:08 +0200)
- 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


No differences found