search

metamath / metamath-knife

Metamath-knife can rapidly verify Metamath proofs, providing strong confidence that the proofs are correct.
Apache License 2.0
25 stars 9 forks source link

Add API to provide "logic" typecode #77

Closed tirix closed 2 years ago

tirix commented 2 years ago

This shall be rather unproblematic, so I'm going ahead and merging it, so I can put it in the v0.3.3 release.

digama0 commented 2 years ago

Actually, this API will need adjustment at some point. There is not necessarily a unique logic typecode or provable typecode.

PS: You misuse the word "shall" a lot. (In the given context it would probably be best to say "this seems to be rather unproblematic" instead.)

tirix commented 2 years ago

Yes, we currently assume there is a single statement of type syntax '|-' as 'wff'; logical typecode, and only support one such statement, but you are right there might be several. I have not checked how MMJ2 handles this. Anyway, let's see when the need arises.

tirix commented 2 years ago

PS: You misuse the word "shall" a lot. (In the given context it would probably be best to say "this seems to be rather unproblematic" instead.)

Thanks! I find I am not assertive enough, and try to correct that, but it looks like I'm overdoing it sometimes! :-) Maybe I could have simply written "should" instead of "shall" ?

digama0 commented 2 years ago

MMJ2 also does not handle multiple logic typecodes well. I only really properly started supporting this situation in the implementation of MM0, but probably we should backport it to the MM proof assistants eventually.

PS: It's not so much about assertiveness, but rather "shall" is a (somewhat dated) alternative form of "will", and is not interchangeable with "should". "Should" would also work in that sentence. (I don't have any issues understanding your English generally but I noticed that you use "shall" in this sense a lot so I thought I would mention it.)