On Friday, January 10, 2020 at 1:52:20 AM UTC+1, Mario Carneiro wrote: > >> we should have guarded the application to avoid seeing it in the first > >> place.
On Fri, Jan 10, 2020 at 5:40 PM Benoit <[email protected]> wrote: > > How would you do that ? (I gave some ideas some time ago on this group, > > but the drawbacks were deemed to outweigh the benefits.) On Fri, 10 Jan 2020 22:18:58 -0500, Mario Carneiro <[email protected]> wrote: > Nothing special; I just mean that any theorem using the expression ( ( S _D > F ) ` x ) should have x e. dom ( S _D F ) in the context or derivable from it. (Mario: I realize you already know this. Benoit: I don't know if you had this in mind.) Another approach for guarding is to use "(New usage is discouraged.)". E.g., add some definition df-XYZ with a construction that's marked "(New usage is discouraged.)", then prove specific properties of it & add them to the "discouraged" file (as permitted uses). From then on, you can depend on the proven properties, but you can't depend on the discouraged details of the construction without specially adding it as a new use (which triggers additional human review). --- David A. Wheeler -- 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/E1iq8RD-0000cP-07%40rmmprod07.runbox.
