function symbols without implementation?

[jwaldmann]

(request for discussion of feature)

It seems an identifier can only be used in axioms and goals if it has a definition (that is, equations).

I would love to be able to have exercises "prove this about f, using only that axioms" - where f's implementation is not given.

Of course, f's type should be declared (see issue #10) but I could also imagine f = undefined

[jwaldmann]

a work-around is to write a definition

append xs ys = append xs ys

cf. https://gitlab.imn.htwk-leipzig.de/waldmann/cyp/commit/88d20eb6cbab06e681bf24339426b845e65893f4

[jwaldmann]

since #22 , we could write

undefined = undefined
append = undefined
reverse = undefined

but I am thinking now that we should not, because by transitivity, we can prove append .=. reverse, which looks dangerous.

https://gitlab.imn.htwk-leipzig.de/waldmann/cyp/commit/59eb3371a844eaf1e0fd160e0475bda9b9dc3f7c

[larsrh]

We can treat undefined as a function and define append and reverse as undefined <some-unique-number>.

[jwaldmann]

Or, some built-in magic: undefined can be used, but it has no "def undefined" rule (or no declaration at all).

I think the ultimate solution is to allow identifiers without implementation (but with type declaration). Then we don't need undefined.

[larsrh]

I'll take a stab.

[larsrh]

Turns out that this is already implemented and you can write

declare_sym append
declare_sym reverse

I forgot that we had this. See 7cb8e90 for the updated bintree test case.