What you could do is, you could create an "opaque" function which gives access to your theorem data. Then wrap that function in an 'annotate form.
(def theorem (f)
(if (check-that-f-is-valid-theorem f)
(annotate 'theorem
(fn (cmd)
(case cmd
get
f
something-else
(do-something-on f))))
(error "Not a valid theorem")))
For that matter, since Arc is around "exploratory programming", in principle Arc will not allow anything that limits what the user can do.
In practice, most users are too busy working on stuff to bother doing something as stupid as (annotate 'theorem something_which_is_not_a_theorem) anyway.
lol
Exploratory programming is fine, but I don't need to explore anymore what a theorem is :-)
> "Arc will not allow anything that limits what the user can do"
Obviously this is not true, as Arc limits me such that I cannot create a safe theorem type. What this means is that I cannot let the user directly interact with Arc when building an interactive theorem prover; I have to wrap some kind of protective layer around it, which would probably hinder lots of the exploring!
