con pattern, visto che in tal caso e' l'intero parsing a dover essere
fatto in un contesto differente. Risolvendo quel bug si risolve
automaticamente anche questo.
con pattern, visto che in tal caso e' l'intero parsing a dover essere
fatto in un contesto differente. Risolvendo quel bug si risolve
automaticamente anche questo.
- theorem t: True. elim x. ==> BOOM! unificazione di una testa flessibile con
True.
- parsing contestuale (tattiche replace, change e forse altre)
- theorem t: True. elim x. ==> BOOM! unificazione di una testa flessibile con
True.
- parsing contestuale (tattiche replace, change e forse altre)
- simplify non debbono zeta-espandere i let-in -> CSC, Gares
- integrare nuova contrib ferruccio nel bench notturno e rilocarla in
contribs o qualcosa del genere -> CSC
- simplify non debbono zeta-espandere i let-in -> CSC, Gares
- integrare nuova contrib ferruccio nel bench notturno e rilocarla in
contribs o qualcosa del genere -> CSC