fact: Definition EvalType (e : Expression) (st : State.t) : Heap.ObjectType := match e with | \type (ReferenceType (TypeDefType cn um)) => (Heap.ObjectObject cn um) | \typeof expr => match EvalRefExpression e st with | Some loc => match Heap.typeof st@h loc with | Some t => t | _ => UndefinedType end | _ => UndefinedType end | _ => UndefinedType end.
imports: Coq(List) Coq(ListSet) Coq(FSetInterface) Coq(Bool) Coq(ZArith) Coq(Relation_Operators) JML(ListHelpers)