<div dir="ltr">Dear Joe and other users,<div><br></div><div>I wonder if in the <kbd><a href="http://www.gilith.com/research/opentheory/article-5-6.html#defineConstListCommand">defineConstList</a> , do you actually define the consts first? Or simply use the const "from construction" [1]. This function is now causing problems in my code and I can't find out where exact the problem is. It would be very nice if you can explain a bit more.</kbd></div><div><kbd><br></kbd></div><div>Thanks a lot.</div><div><kbd><br></kbd></div><div><kbd><br></kbd></div><div><kbd>[1] By this, I mean, did you used defineConst or anything to do the definition for individual constants there or simply getting the list pushed as</kbd></div><a name="defineConstListCommand" style="color:rgb(0,0,0);font-family:sans-serif;font-size:medium"><blockquote style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex" class="gmail_quote"></blockquote></a>> List [Const c1, ..., Const ck]<div><br><div>--</div><div><div class="gmail_signature"><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><br></div><div>Regards,</div><div><a href="http://www.dptinfo.ens-cachan.fr/~swang/" target="_blank">Robert White </a>(Shuai Wang)</div><div><a href="https://www.rocq.inria.fr/deducteam/" target="_blank">INRIA Deducteam</a></div></div></div></div></div></div></div></div></div>
</div></div></div>