fact: Definition rewriteMethod (m:Method) (enc:TYPEDEF.t) : Method := let specs0 := rewriteFullSpecification (METHOD.fullSpecs m) m enc in METHOD.setSpecs m specs0.
imports: JML(Prelude) Coq(ZArith) Coq(Bool) Coq(List) JML(TaggedList) JML(ListHelpers) JML(ListFunctions) JML(OptionHelpers) JML(JMLProgramPlusImpl) JML(JMLFull2Basic) JML(JMLExpressionNotations)