fact: Definition mint_eval (val : valuation I) k (mi : mint k) : vec := let coefs := Vbuild (fun i (ip : i < k) => dom2vec (val i)) in add_vectors (Vcons (AMatrixBasedInt.const mi) (Vmap2 mat_vec_prod (args mi) coefs)).
imports: CoLoR(Matrix AMonAlg VecUtil OrdSemiRing ATrs LogicUtil RelUtil NatUtil AWFMInterpretation) Coq(PeanoNat Setoid Morphisms)