fact: Definition modelField (e:t) (sfn:ShortModelFieldName) : option ModelField := let eq_sfn (f:ModelField) := Z_eqb (FIELDSIGNATURE.name (MODELFIELD.signature f)) sfn in List.find eq_sfn (modelFields e).
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)