On Fri, Oct 18, 2019 at 3:29 PM Olivier Binda <[email protected]> wrote:
> I have started looking at the Peano file and understanding mm0. > > This looks a lot like function signatures, with abstract/concrete bodies. > So Mephistolus statements like "( v1w -> v2w )" might be viewed as a > function im (v1w v2w : wff) : wff = $( v1w -> v2w )$ > That depends on what you mean. A "term" or "def" is used to define a new expression constructor, like implication. That looks like this: term im: wff > wff > wff; infixr im: $->$ prec 25; That declares implication as a right arrow (right associative), and from this point on you are permitted to write things like "v1w -> v2w" in statements. It is basically the equivalent of metamath's wi $a wff ( ph -> ps ) $. statement. This is by contrast to theorem statements and hypotheses, which in metamath usually come after a "|-" symbol. In MM0 these appear in "axiom" and "theorem" statements, like this one: theorem syl (a b c: wff) (h1: $ a -> b $) (h2: $ b -> c $): $ a -> c $; This says that given proofs of a -> b and b -> c, we get a proof of a -> c. In MM0 this ends right away with a semicolon, and in MM1 the proof is given afterwards as a lisp expression: theorem syl (a b c: wff) (h1: $ a -> b $) (h2: $ b -> c $): $ a -> c $ = (proof...); These are exactly analogous to the theorems that take up the majority of the space in MM databases like set.mm. -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSudWF%3Do5MzERFqFNXRRLZbqfaH%2BTb9J_%3DTgG%2B0Rqsyd7A%40mail.gmail.com.
