[opentheory-users] removing definitions from theories

[Joe Leslie-Hurd]

Hi Ramana,

There's currently no tool support for this, but I don't think it would
be too difficult to implement. What is your use-case?

Cheers,

Joe

On Fri, Jan 29, 2016 at 12:36 AM, Ramana Kumar <ramana at member.fsf.org> wrote:
> Hi,
>
> Is it possible to take a theory that makes definitions of types/constants,
> and then re-present the same theory _without_ making the definitions
> (instead taking them as ungrounded constants, and the definitional theorems
> as axioms).
>
> I know there is already this command:
>
> opentheory info --theorems ...
>
> which removes all the proofs, but it still keeps the definitions in.
>
> Can I also remove the definitions?
>
> In essence, I want a totally axiomatic presentation of a theory.
>
> Thanks,
> Ramana
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>