search

digama0 / mm0

Metamath Zero specification language
Creative Commons Zero v1.0 Universal
312 stars 40 forks source link

signature of a def for df_sb #143

Closed Lakedaemon closed 3 months ago

Lakedaemon commented 3 months ago

Hello Mario

What should be the signature of df_sb if it were turned into a mm0 def ? Would it be {x,.y:set} (ph : wff x) (t : set): wff t ?

Or something completely different ?

I'm in the process of turning metamath definitions into mm0 definitions

(to be on the safe side, my software is using mm0 with metamath theorems, with only some new nodes converting trees to more convenient nodes (somewhat like def does)

I have been helped so far by set.mm0 (many thanks for that) but now I have to go beyond....

Best regards, Olivier

Lakedaemon commented 3 months ago

I think that I got the hang of it...

Implementing metamath definitions (df- ) with mm0 syntax like crazy now