[CakeML] Behaviour of evaluate_dec

Lars Hupel hupel at in.tum.de
Mon May 29 07:41:30 UTC 2017


> 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.

I see. Is the following use case supported somehow:

I want to go through a list of declarations (containing only types and
let rec) and observe the resulting cumulative environment env', starting
with an empty environment. I then want to prove some properties about
evaluation of expressions in env'.

Cheers
Lars



More information about the Users mailing list