Reveal lemmas are not copied from traits to extending classes, leading to resolution errors

[cpitclaudel]

trait T {
  predicate {:opaque} True() { true }
}

class C extends T {}

bug.dfy(5,6): Error: class 'C' does not implement trait lemma 'T.reveal_True'

(CC @fabiomadge FYI)

[fabiomadge]

I think that's by design.

dafny/Source/Dafny/Rewriter.cs

Line 1053 in 3ae2167

} else if (!RefinementToken.IsInherited(function.tok, c.EnclosingModuleDefinition)) {

[cpitclaudel]

I wonder if that was instead due to some code that previously copied those, so that they wouldn't be regenerated?

[MikaelMayer]

My workaround:

trait T {
  predicate {:opaque} True() { true }
}

class C extends T {
  lemma reveal_True() {}
}