get rid of axiomatized by in favor of [opaque] with trivial lemma

[oskgo]

Note that this does not fully deprecate axiomatized by yet. It only removes its uses from the stdlib.

Ref: #94

[oskgo]

I can't check examples/MEE-CBC/FunctionalSpec.ec locally. CBC doesn't find FMap for some reason. Any idea about this?

I'll make the fixes anyways and use CI to check them instead though.

[strub]

With make check?

[oskgo]

make check is picking up a lot of errors from emacs temp files and won't get to the examples, but I'll try to get it working.

[strub]

make check is picking up a lot of errors from emacs temp files and won't get to the examples, but I'll try to get it working.

This should not be the case. Could you file an issue with more details?

[oskgo]

Using make check seems to work once I've removed all the .#Theory.ec files, but I'd like to note that the developer experience of having to re-check every single theory for a single fix in a single file is not great. Is there something I'm doing wrong or is this just how the stdlib works?

[strub]

That's sub-optimal, I agree. This is because make check disables .eco generation. But we should change this.