Hello,
In the metamath book, p114 there is this assertion :
The type declared by a *$f *statement for a given label is global even if
the
variable is not (e.g., a database may not have *wff P * in one local scope
and
*class P* in another).
I can guess the justification was to speed up verification of types with no
soundness weakness, but it seems not to be inforced in metamath-exe :
this minimal example doesn't trigger an error message (variable v is
declared with types A then B, and used in both proofs).
So should we add an erratum to he book errata list, or file an issue to
metamath-exe ?
================
$c A B $.
${
$v v $.
tA $f A v $.
hypA $e A v $.
conA $p A v $= hypA $.
$}
${
$v v $.
tB $f B v $.
hypB $e B v $.
conB $p B v $= hypB $.
$}
--
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 visit
https://groups.google.com/d/msgid/metamath/28eca871-e707-4f44-af32-f2d552b767d0n%40googlegroups.com.
