Open gmalecha opened 7 years ago
We have a lot of duplicate code for various pieces of the automation, e.g. polymorphic lemmas for PAPPLY and polymorphic lemmas for rewriting. All of these should be combined and the associated proofs should be de-duplicated.
Given the poor performance of polymorphic apply in the CPP paper, it might be necessary to special-case non-polymorphic lemmas.
We have a lot of duplicate code for various pieces of the automation, e.g. polymorphic lemmas for PAPPLY and polymorphic lemmas for rewriting. All of these should be combined and the associated proofs should be de-duplicated.