<div dir="ltr"><div>Hi Lars,<br><br></div>That sounds like what the HOL-to-CakeML translator does. You might want to look at the translator/ directory, and at Magnus and Scott's ICFP/JFP paper: <a href="https://cakeml.org/jfp14.pdf">https://cakeml.org/jfp14.pdf</a><br><br>Specifically, I think ml_translatorScript (Eval_def) does it for expressions and mlProgScript lifts it up to decs.<br></div><div class="gmail_extra"><br><div class="gmail_quote">On Mon, May 29, 2017 at 3:41 AM, Lars Hupel <span dir="ltr"><<a href="mailto:hupel@in.tum.de" target="_blank">hupel@in.tum.de</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class="">> The c field is for new data constructors. let rec doesn’t make any new data constructors, so it is empty. The result for each declaration (for both variables and constructors) is not cumulative, but just the definitions that that declaration makes.<br>
<br>
</span>I see. Is the following use case supported somehow:<br>
<br>
I want to go through a list of declarations (containing only types and<br>
let rec) and observe the resulting cumulative environment env', starting<br>
with an empty environment. I then want to prove some properties about<br>
evaluation of expressions in env'.<br>
<div class="HOEnZb"><div class="h5"><br>
Cheers<br>
Lars<br>
<br>
______________________________<wbr>_________________<br>
Users mailing list<br>
<a href="mailto:Users@cakeml.org">Users@cakeml.org</a><br>
<a href="https://lists.cakeml.org/listinfo/users" rel="noreferrer" target="_blank">https://lists.cakeml.org/<wbr>listinfo/users</a><br>
</div></div></blockquote></div><br></div>