I put up a PR for your consideration. https://github.com/githwxi/ATS-Postiats/pull/170
On Tuesday, July 4, 2017 at 2:47:15 PM UTC-4, Steinway Wu wrote: > > I encountered a problem. > > Say I have this in the ATS code > > stacst set_emp: set = "ext@smt_set_emp" > > and this in the smt2 code > > (define-const smt_set_emp (Set) ((as const (Set)) false)) > > `--constraint-export` is able to translate all static applications of > `smt_emp` to `smt_set_emp`. > > *However, it emits an extra definition which I don't want to have.* > > (declare-fun smt_set_emp () Set) > > What is your usual use case? Maybe we should remove this from emitted > code. > > On Wednesday, June 29, 2016 at 1:24:12 PM UTC-4, gmhwxi wrote: >> >> >> In ATS2-0.2.8, a static constant can now be declared with an external >> name: >> >> For instance: >> >> stacst sine_of_real : real -> real = "ext#sin" >> >> This is useful when constraints generated during typechecking are to be >> exported >> for solving externally. If a static constant is given an external name, >> then the external >> name is used in exported constraints (otherwise, a name like >> sine_of_real!12345 is >> used, where 12345 is the stamp attached to the static constant). >> >> Here are some examples that you can try (using the given Makefile): >> >> >> https://github.com/githwxi/ATS-Postiats-contrib/tree/master/projects/MEDIUM/ATS-extsolve/ATS-extsolve-smt2/TEST >> >> Cheers! >> >> -- You received this message because you are subscribed to the Google Groups "ats-lang-users" group. To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-users+unsubscr...@googlegroups.com. To post to this group, send email to ats-lang-users@googlegroups.com. Visit this group at https://groups.google.com/group/ats-lang-users. To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/99550848-6084-4b66-bb3c-4dbaa3104de7%40googlegroups.com.
