Email Gateway (Aug 22 2022 at 10:21): Email Gateway (Aug 22 2022 at 10:21):From: Peter Lammich <lammich@in.tum.de>
Hi List.
Consider the following theory, where I use the of and where attributes
to instantiate a variable to "TYPE(nat)".
Without Eisbach included, everything is fine. With Eisbach included, I
get the error "Lost indexname in instantiated theorem".
What is going on here, and is there a workaround?
Email Gateway (Aug 22 2022 at 10:22):From: Peter Lammich <lammich@in.tum.de>
Consider the following theory, where I use the of and where attributes
to instantiate a variable to "TYPE(nat)".
Without Eisbach included, everything is fine. With Eisbach included, I
get the error "Lost indexname in instantiated theorem".What is going on here, and is there a workaround?
A possible workaround (except from not using Eisbach) is to use
"Pure.of"/"Pure.where" instead of "of"/"where".
Email Gateway (Aug 22 2022 at 10:26):From: Daniel Matichuk <daniel.matichuk@nicta.com.au>
Hi Peter,
Eisbach shadows the existing "of" and "where" attributes to support being re-interpreted in method expressions (which it looks like you've figured out).
What you're seeing is an error in this additional functionality, specifically it decides that "TYPE(nat)" means that you want to instantiate a type attribute to "nat". This results in some inconsistency when forming a static closure.
This should be easy to fix. The easiest workaround in the interim is to avoid using bare "TYPE('a)".
i.e.
thm foo[of "id TYPE(nat)",simplified id_def]
Which I realise is a bit of a pain (sorry about that). Using "Pure.of" is also fine as long as you aren't defining an Eisbach method.
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Last updated: Apr 26 2024 at 16:20 UTC