Skip to content

enable name-mangling-light

Ralf Jung requested to merge ralf/mangled into master

For instance, the proof state after the intros. in lookup_total_app_l now looks like

  A : Type
  __Inhabited : Inhabited A
  l1, l2 : list A
  i : nat
  __H : i < length l1
  ============================
  (l1 ++ l2) !!! i = l1 !!! i

I like it. :) I think we can just always enable this and not have anything extra on CI; we will hopefully notice when proof scripts contain such an identifier starting with __.

Merge request reports