Hi is there an answer to this question? On Monday, June 5, 2023 at 1:43:41 PM UTC+8 Humanities Clinic wrote:
> 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/dcffc310-0cfa-4ef6-9f8d-604e00faae72n%40googlegroups.com.
