fact: Fixpoint ei2i (e:ExprI) : int := match e with | EI0 => 0 | EI1 => 1 | EI2 => 2 | EI3 => 3 | EIadd e1 e2 => (ei2i e1)+(ei2i e2) | EIsub e1 e2 => (ei2i e1)-(ei2i e2) | EImul e1 e2 => (ei2i e1)*(ei2i e2) | EImax e1 e2 => max (ei2i e1) (ei2i e2) | EIopp e => -(ei2i e) | EIraw i => i end.
imports: BinInt