An implementation is now found here with documentation and examples.
The name is admittedly a bit of mischief: I am Holmes, I already have a prover called Watson, and my son suggested that I call this one Lestrade...
Here is the source for the implementation in Moscow ML 2.01 of the Lestrade Type Inspector. As of 10/14/2017 this differs by one character from a LaTex document here (literate programming attempted): the idea is that I can maintain a readably commented source in this way.
It is no longer necessary to contain different versions for different flavors of ML: there is a preamble which one can modify to run Lestrade under PolyML or Moscow ML 2.10. The latest update streamlines the behavior of the rewrite commands; if any old scripts have the old rewrite command format, the version lestrade-9-17-17.sml still understands the old forms.
Here is my scratch work as I read through Mike Nahas's Coq tutorial and prove analogous things under Lestrade.
Here is a paper I am working on in summer 2016, containing an outline of the philosophical approach, an account of the commands and the formal language of Lestrade, and extensive sample Lestrade books. This is the best current approximation to a manual
Here are the slides (slightly improved) for the talk I gave to the Boise State logic seminar Oct 24 2017. Here is an older set of slides (misleadingly also dated Oct 24 due to the date function of LaTeX).
Here is a paper I am working on in fall 2017, simultaneously an account of Lestrade and a treatment of foundational topics; it is another pass at the aims of the paper just below, and discusses new additions to the capabilities of Lestrade.
Here is a paper I am working on in summer 2017, simultaneously an account of Lestrade and a treatment of foundational topics.
Here is a paper I am working on in fall 2017, outlining implementation of homotopy type theory under Lestrade. I'm not finished with this by any means, it is rather tricky.
Here is an axiomatization of ZFC in Lestrade. Not of much interest until I prove something with it!
Here is a paper I am working on in fall 2017, exhibiting the rewriting capabilities, and the ability to use rewrite rules provably valid in a theory to implement programming behavior: the file is intended to support computation of Fibonacci numbers (thus the name) but at the moment supports a fully implemented adder for binary numerals on top of a simple theory of arithmetic: all of its computations are theorems. The rewrited command, not witnessed so far in other files, is used extensively in this one.
Here is another paper I am working on in summer 2016, focussed more narrowly on the philosophical approach.
And here is another paper I am working on in fall 2016, which pretends to be an initial segment of an elementary discrete math test supported by Lestrade text.
Here is the source for the implementation in Moscow ML 2.01 of a version of Lestrade without the new type inference capabilities, which I will continue to maintain. I'll leave this up, but maintenance of it is suspended: the main version now supports a command basic() which will give this behavior, and fullversion() to restore type inference functions.
Here are the slides for a talk I am giving locally on October 25th 2016. Here is the supporting Lestrade script file.
Here is an old manual (which I updated for a while but which doesn't have the latest changes; it does not say everything that the paper designated as the manual above says, but it has a different emphasis and I think it might still be useful).
Here is Freek Wiedijk's Automath site, including the only currently available implementation of standard Automath (as far as I know). What I present here is not standard Automath!
Here is the official Automath archive site.