Proof values: is there an equality/inequality operator?

Google Group
1

Given this (an example):

dataprop NAT =
| ZERO
| SUCC of NAT

prval pf1 = SUCC(SUCC(ZERO))
prval pf2 = SUCC(SUCC(ZERO))

is there any way to say pf1 is equal to pf2?

It tried this, naively:

prval equal = (pf1 = pf2)

but it does not work, as ATS complains it can’t resolve the operator.

I believe this makes sense with dataprop.

2

A proof is dynamic. There is no built-in equality on dynamic values.

You can have something like:

dataprop NAT(int) =
| Z(0)
| {n:nat} S(n+1) of NAT(n)

extern
prfun NAT_EQ: {m,n:nat} (NAT(m), NAT(n)): bool(m==n)

implement NAT_EQ(pf1, pf2) =
case+ (pf1, pf2)
| (Z(), Z()) => true
| (S(pf1), S(pf2)) => NAT_EQ(pf1, pf2)
| (_, _) =>> falseOn Fri, Dec 18, 2015 at 12:59 PM, ‘Yannick Duchêne’ via ats-lang-users < ats-lan...@googlegroups.com> wrote:

Given this (an example):

dataprop NAT =
| ZERO
| SUCC of NAT

prval pf1 = SUCC(SUCC(ZERO))
prval pf2 = SUCC(SUCC(ZERO))

is there any way to say pf1 is equal to pf2?

It tried this, naively:

prval equal = (pf1 = pf2)

but it does not work, as ATS complains it can’t resolve the operator.

I believe this makes sense with dataprop.

–
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-user...@googlegroups.com.
To post to this group, send email to ats-lan...@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/a0d700ae-489a-4520-8d60-4328f5f26466%40googlegroups.com
https://groups.google.com/d/msgid/ats-lang-users/a0d700ae-489a-4520-8d60-4328f5f26466%40googlegroups.com?utm_medium=email&utm_source=footer
.

3

So it has to be user defined.

In a way, that make sense too, as proof values can be made up of dynamic
values, indeed, although a proof constructor can be defined without any
reference to any dynamic value, that’s just a special case, so there can’t
be a general comparison operator.Le vendredi 18 décembre 2015 19:14:19 UTC+1, gmhwxi a écrit :

A proof is dynamic. There is no built-in equality on dynamic values.

You can have something like:

dataprop NAT(int) =
| Z(0)
| {n:nat} S(n+1) of NAT(n)

extern
prfun NAT_EQ: {m,n:nat} (NAT(m), NAT(n)): bool(m==n)

implement NAT_EQ(pf1, pf2) =
case+ (pf1, pf2)
| (Z(), Z()) => true
| (S(pf1), S(pf2)) => NAT_EQ(pf1, pf2)
| (_, _) =>> false

On Fri, Dec 18, 2015 at 12:59 PM, ‘Yannick Duchêne’ via ats-lang-users < ats-l...@googlegroups.com <javascript:>> wrote:

Given this (an example):

dataprop NAT =
| ZERO
| SUCC of NAT

prval pf1 = SUCC(SUCC(ZERO))
prval pf2 = SUCC(SUCC(ZERO))

is there any way to say pf1 is equal to pf2?

It tried this, naively:

prval equal = (pf1 = pf2)

but it does not work, as ATS complains it can’t resolve the operator.

I believe this makes sense with dataprop.

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...@googlegroups.com <javascript:>.
To post to this group, send email to ats-l...@googlegroups.com
<javascript:>.
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/a0d700ae-489a-4520-8d60-4328f5f26466%40googlegroups.com
https://groups.google.com/d/msgid/ats-lang-users/a0d700ae-489a-4520-8d60-4328f5f26466%40googlegroups.com?utm_medium=email&utm_source=footer
.