[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