hax into lean

Stream: Program verification

[Oliver Butterley]

Sometimes the names of extracted functions in lean contain Impl_7 and similar although this wasn't present in the source code. Where does this come from? @Clément Blaudeau

[Clément Blaudeau]

Those are disambiguators for otherwise "anonymous" implementations, as one can have several implementations attached to the same type :

struct S {}

impl S {
    fn f1 () {}
}

impl S {
    fn f2 () {}
}

[Oliver Butterley]

Thanks for the clarification