Proof values: is there an equality/inequality operator?

[Yannick Duchêne]

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`.

[Hongwei Xi]

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

--
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.

[Yannick Duchêne]

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.