We can inline pre/post conditions in the contracts of traits. Then we can disable the spec-trait phase in Lean and these checks are probably no longer needed:
|
item.ident.is_precondition() || item.ident.is_postcondition() || |
|
item.ident.is_precondition() || item.ident.is_postcondition() || |