Skip to content
  • Robbert Krebbers's avatar
    More consistent naming for fixpoints. · b60e126a
    Robbert Krebbers authored
    - Use Φ and Ψ for predicates.
    - Use _1 and _2 suffixes for the different directions of a lemma.
    - Not all lemmas started with _uPred; we do not let the bigop lemmas (for instance)
      start with uPred_ either, so I just got rid of the prefix.