Version 0.3
Version 0.2
-
Output from LNgen now integrates for more nicely with the output
from Ott. In fact, the output from LNgen must be combined with the
output from Ott in order for everything to work. For this all to
work, however, you must patch Ott and structure your input files in
a particular way. Details are in the README file that comes with
the distribution.
-
Output from LNgen now works with "the
regular" metatheory
library, not a customized version that departs radically from
previous releases of the library.
-
LNgen now accepts additional command-line arguments, in particular,
one to admit all generated lemmas (useful during language
development to avoid repeated recompilation).
-
LNgen, in concert with Ott, now generates separate definitions of
local closure predicates for
Set and Prop,
as opposed to only Set in the previous release. The
two version are proved equivalent to each other. Most lemmas are
proved for the version in Prop.
-
LNgen now generates statements and proofs of more lemmas.
Version 0.1