I've written a Haskell program that acts as a conversion between Norrish numerals and binary numerals. It reads an OpenTheory article encoding a Norrish numeral n[N] (made with bit1, bit2, and zero) and writes an article that proves the theorem: |- n[N] = n[B] where n[B] is the binary encoding of n (made with bit0, bit1, and zero). You can access it as a "standalone tactic" at <a href="http://cam.xrchz.net/n2b.cgi">http://cam.xrchz.net/n2b.cgi</a>. It may use up to 6 theorems as axioms (which are all proved in the standard library). The Haskell source code is here <a href="https://github.com/xrchz/typed-conv/blob/master/numeral/n2b.hs">https://github.com/xrchz/typed-conv/blob/master/numeral/n2b.hs</a> (around 500 lines). I'm pretty new to Haskell, so I'd very much appreciate any comments on the design. A lot of the infrastructure should be resuable by future standalone tactics in Haskell. 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 - would it be more efficient to store conclusions with proofs rather than computing them with concl? but I think Haskell memoises anyway... - is there a better algorithm for converting between these numeral encodings? - my articles always leave tonnes of stuff on the stack because they just def everything... is there an efficient algorithm for only deffing things you'll actually use (and maybe removing them after you won't any more)? - probably lots of obvious things I'm doing less nicely than is possible...