On Sun, May 8, 2022 at 8:17 AM Glauco <[email protected]> wrote:
> I've not looked at the spec in the metamath book, yet, to see if actually > any var is required to have a kind (when used in assertions). > To this question specifically: Yes, every variable appearing in a $a statement must have an $f in scope. From the book (p.114): > A $f, $e, or $d statement is active from the place it occurs until the end of the block it occurs in. > A $a or $p statement is active from the place it occurs through the end of the database. > There may not be two active $f statements containing the same variable. > Each variable in a $e, $a, or $p statement must exist in an active $f 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/CAFXXJStFG7TEMiM805gZPd-1xOuFjJeBgOjjdRVU%3Dkknth6E%2Bw%40mail.gmail.com.
