formula_type_binder

[Lakedaemon]

I do not get what case this is used for (in theorems/axioms for mm0) : identifier_ : formula Could you please explain, with an example ?

[Lakedaemon]

Is it to say something like ( x : $ 2 * y + 1$ ) to say that x is equal to 2y+1

instead of putting this inside an hypothesis ?

$ y = 2 * x + 1 $ >

[Lakedaemon]

could you please explain ?

[digama0]

Oh, sorry my browser must have eaten the response. The notation foo > is exactly equivalent to a binder of the form (_: foo). That is, it is a binder with no name, meaning that it cannot be referred to later because _ is not an identifier, but otherwise is equivalent to any other binder like (a: foo). This applies for both regular binders and hypothesis binders, but in mm0 files the names of hypothesis binders are irrelevant, so the $ foo $ > form is simpler. In proof files (both mm1 and mmu), the names of hypothesis binders are the way to apply the hypothesis inside the proof.

[digama0]

To your example, the equivalent of $ y = 2 * x + 1 $ > is (h: $ y = 2 * x + 1 $), where h is now naming a hypothesis that can be used in the proof to assert that y = 2 * x + 1.