fact: Definition findField (p : Program) (fd : FieldSignature) : option Field := let (cn, sfs) := fd in match PROG.class p cn with | None => None | Some cl => CLASS.field cl (FIELDSIGNATURE.name sfs) end.
imports: JML(JMLProgramPlus) Coq(ZArith) JML(ZHelpers) JML(LogicHelpers) Coq(Bool) Coq(Sumbool) Coq(Ndec) JML(PosAux) JML(EqBoolAux) Coq(Relation_Operators) Coq(List) JML(ListFunctions) JML(ListHelpers) JML(OptionHelpers)