fact: Definition vm_of_list T (l : list T) : VarMap.t T := let fix aux acc p l := match l with | [::] => acc | x :: l => aux (VarMap.vm_add x p x acc) (Pos.succ p) l end in aux VarMap.Empty 1%positive l.
imports: elpi(elpi) Coq(QArith Ring) Coq.micromega(RingMicromega QMicromega EnvRing Tauto Lqa) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(fintype finfun bigop order ssralg ssrnum ssrint) mathcomp.zify(ssrZ zify) mathcomp.algebra_tactics(common)