[opentheory-users] a standalone tactic translating numeral encodings

[Joe Hurd]

Hi Ramana,

This is extremely impressive work - nice job!

By the way, I tried calling it from HOL Light but couldn't make it
work - does it use your standard convention that the conversion
accepts an axiom of the form `K F n[N]` and returns a theorem of the
form `|- n[N] = n[B]`? My attempt is at the bottom of the file
opentheory/cloud.ml in my HOL Light fork.

> Specific design questions I have:
>  - would it be better to somehow write articles without going via a type of
> proofs (i.e. just directly log as theorems are built)? I tried to figure out
> a way to do that but failed, and also stopped thinking it would be better

I like the way you have it right now with a datatype of proofs.

>  - would it be more efficient to store conclusions with proofs rather than
> computing them with concl? but I think Haskell memoises anyway...

My gut reaction is that this would be a false economy. It's much
clearer the way you have it now.

>  - is there a better algorithm for converting between these numeral
> encodings?