Renaming predicates in program-to-program verification #71
Labels
A-verifying
Area: Verifying
C-enhancement
Category: Enhancement
E-medium
Experience: Medium
L-fol
Language: First-order logic
P-high
Priority: High
Currently, predicate renaming always occurs (but it doesn't have to). We need to settle on cases when renaming isn't necessary with the goal of making lemma writing easier (e.g. don't have to name a predicate p as p_1 or p_2 when writing lemmas).
The text was updated successfully, but these errors were encountered: