fact: Definition EvalModelFieldAccess (fsig : ModelFieldSignature) (target : option Expression) (st : State.t) : option Value := match target with | Some target' => match EvalRefExpression target' st with | None => None | Some loc => EvalModel p fsig (Some loc) st end | None => EvalModel p fsig None st end.
imports: Coq(List) Coq(ListSet) Coq(FSetInterface) Coq(Bool) Coq(ZArith) Coq(Relation_Operators) JML(ListHelpers)