<div dir="auto">Common problems include:<div dir="auto">- The spec theorem has type variables that need instantiation,</div><div dir="auto">- The function is not in scope,</div><div dir="auto">- The function is applied to the wrong number of arguments</div><div dir="auto"><br></div><div dir="auto">I think the middle one can reduce your goal to false whereas the others can raise exceptions. Does your p variable have 'ffi ffi_proj type?</div><div dir="auto"><br></div><div dir="auto">I'll try to have a look at some point. (Currently at AITP.)</div></div><div class="gmail_extra"><br><div class="gmail_quote">On 25 Mar 2017 20:09, "Yong Kiam" <<a href="mailto:tanyongkiam@gmail.com">tanyongkiam@gmail.com</a>> wrote:<br type="attribution"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">Those tactics are defined in the tactic libs in characteristic/, I fixed a few issues back on env-refactor by stepping through them.<br></div><div class="gmail_extra"><br><div class="gmail_quote">On Sat, Mar 25, 2017 at 2:46 PM, Scott Owens <span dir="ltr"><<a href="mailto:S.A.Owens@kent.ac.uk" target="_blank">S.A.Owens@kent.ac.uk</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Ok. I think I have the dependencies right now. However, I still have 4 cf_apps where xapp and xapp_spec fail, and I have no idea why, or how to even start debugging the problem. This is on the sort_example branch, characteristic/examples/sortPr<wbr>ogScript.sml. Any hints would be greatly appreciated.<br>
<span class="m_-195553722216766323HOEnZb"><font color="#888888"><br>
Scott<br>
</font></span><div class="m_-195553722216766323HOEnZb"><div class="m_-195553722216766323h5"><br>
> On 2017/03/25, at 02:46, Ramana Kumar <<a href="mailto:Ramana.Kumar@cl.cam.ac.uk" target="_blank">Ramana.Kumar@cl.cam.ac.uk</a>> wrote:<br>
><br>
> Add arrays into the same linear sequence that includes I/O and update the basis/dependency-order file accordingly.<br>
><br>
> The longer term solution is to get the abstract translator working. (There is an issue, and was some discussion on a wiki page.)<br>
><br>
> On Friday, 24 March 2017, Scott Owens <<a href="mailto:S.A.Owens@kent.ac.uk" target="_blank">S.A.Owens@kent.ac.uk</a>> wrote:<br>
> > I’m trying to verify a program with CF that uses both arrays and I/O from the basis. I don’t see how to make this work, since you only seem to be able to do 1 translation_extends. Any ideas?<br>
> ><br>
> > Scott<br>
> > ______________________________<wbr>_________________<br>
> > Developers mailing list<br>
> > <a href="mailto:Developers@cakeml.org" target="_blank">Developers@cakeml.org</a><br>
> > <a href="https://lists.cakeml.org/listinfo/developers" rel="noreferrer" target="_blank">https://lists.cakeml.org/listi<wbr>nfo/developers</a><br>
> ><br>
<br>
______________________________<wbr>_________________<br>
Developers mailing list<br>
<a href="mailto:Developers@cakeml.org" target="_blank">Developers@cakeml.org</a><br>
<a href="https://lists.cakeml.org/listinfo/developers" rel="noreferrer" target="_blank">https://lists.cakeml.org/listi<wbr>nfo/developers</a><br>
</div></div></blockquote></div><br></div>
</blockquote></div></div>