search

expln / metamath-lamp

Metamath-lamp (Lite Assistant for Metamath Proofs) is a GUI-based proof assistant for creating formal mathematical proofs in Metamath that does not require installation (just run it directly using your web browser).
https://expln.github.io/lamp/latest/index.html
MIT License
13 stars 5 forks source link

Add transitively skipped assertions option #152

Closed CatsAreFluffy closed 1 year ago

CatsAreFluffy commented 1 year ago

For example, if I was trying to prove a theorem without using ~ ax-rep, I would want to skip not just ax-rep, but all theorems using ax-rep.

expln commented 1 year ago

Ok, that makes sense. I will implement it.

expln commented 1 year ago

This is implemented on dev.

Please read this comment to understand the new settings which allow to skip some assertion and all the theorems depending on it.

In order to skip ax-rep and all theorems using ax-rep, you may set the new settings as follows:

image