Prfun, extern and implement

Google Group
1

Hi,

In ATS1, I saw things like this

“extern prfun foo…”
“implement foo … = …”

Is that changed in ATS2? I got weird error message saying “dynamic constant
implementation need to be non-proof”.

Thanks,

(And, I suggest adding a tag “proof”)

2

For implementing a proof function, you need to use the keyword
primplmnt or primplementOn Thursday, November 6, 2014 5:05:41 PM UTC-5, hw…@bu.edu wrote:

Hi,

In ATS1, I saw things like this

“extern prfun foo…”
“implement foo … = …”

Is that changed in ATS2? I got weird error message saying “dynamic
constant implementation need to be non-proof”.

Thanks,

(And, I suggest adding a tag “proof”)