prfun, extern and implement

[hw...@bu.edu]

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")

[gmhwxi]

For implementing a proof function, you need to use the keyword
primplmnt or primplement