Hihi, I have read most of Dr Megill/Wheeler's Metamath book, as well as most of the MPE pages, and I understand that typecodes are used to specify the type of a variable in $f statements.
(1) How and when does Metamath ensure the types are "enforced"? When does it throw an error? (Oh, please do let me know which part of Dr Megill/Wheeler's book has the answer if I have missed it.) (2) Also, I know $e, $a, $p statements all have typecodes as well. Are their type codes enforced/used in the same way as $f statements? (3) And, am I right to say that a type code can just be *any* constant? ie declared in $c statement? -- 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/007a8041-d7ed-4549-9621-3f7ec63dd45fn%40googlegroups.com.
