search

tirix / rumm

A tactics-based Metamath proof language
5 stars 3 forks source link

Update specification #17

Closed GinoGiotto closed 3 months ago

GinoGiotto commented 4 months ago

I added a few details and described the missing features from the specification. Every provided example is "functional", meaning it generates a complete proof when executed by Rumm. The proofs are borrowed from set.mm, allowing users to consult them from the explorer, while examining the example tactics. The proofs are also meant to be minimal, to make the examples easier to understand.

GinoGiotto commented 3 months ago

Btw, it seems there are also the import keyword and the include keyword, although I don't know what they do @tirix.

https://github.com/tirix/rumm/blob/1ab8d60a929d0788bc02b590a06b7eebd011a66c/rumm/src/parser.rs#L28-L32

I'm only aware of the load keyword because that is used in set.rmm.

tirix commented 3 months ago

the import keyword and the include keyword

They are just provisions for loading third party files, none of them currently works.

GinoGiotto commented 3 months ago

Ok, then this PR contains most of what I'm aware of, unless there are some other obscure features that I missed.

GinoGiotto commented 3 months ago

@tirix Is this PR good for you? If addressed, I will close issue #14, since the s/ keyword would be in the specification. To keep topics in order, I will also link the bug mentioned in https://github.com/tirix/rumm/issues/14#issuecomment-2252416998 in issue https://github.com/tirix/rumm/issues/13, since they likely have the same origin (it would be nice to have #13 fixed, since it would eliminate the need for work variables).

tirix commented 3 months ago

Yes, let's merge this!