Metamath-lamp version 17 released

51 views
Skip to first unread message

Igor Ieskov

unread,
Aug 28, 2023, 2:46:42 PM8/28/23
to Metamath
Metamath-lamp version 17 includes the following updates:

The major update is how mm-lamp handles discouraged assertions. Discouraged assertions were supported in the previous versions too, but in version 17 it became more convenient. Also, assertions can be marked as "deprecated". This allows to exclude them from proofs independently of "discouraged" ones. More details on that may be found in the below issues:

"By default ignore any statements marked (New usage is discouraged.)" https://github.com/expln/metamath-lamp/issues/31#issuecomment-1682725469

"By default don't use discouraged syntax nor later syntax" https://github.com/expln/metamath-lamp/issues/108

"Add transitively skipped assertions option" https://github.com/expln/metamath-lamp/issues/152

And few minor changes:

"In explorer allow selection of final type" https://github.com/expln/metamath-lamp/issues/111

"Duplicate up button" https://github.com/expln/metamath-lamp/issues/154

"When substituting, always use the most recent selections" https://github.com/expln/metamath-lamp/issues/155

-
Igor
Reply all
Reply to author
Forward
0 new messages