Email Gateway (Aug 19 2022 at 15:12): Email Gateway (Aug 19 2022 at 15:12):From: Lars Hupel <hupel@in.tum.de>
Hi,
assume this simple inductive definition:
inductive foo :: "nat ⇒ bool" where
foo1: "foo 0"
Now, trying the completion:
thm foo<Ctrl-B>
... this gives me "foo.cases", "foo.induct", ... (as expected), and also
"foo1". It doesn't give me "foo.foo1", though.
Peter suggested that the general policy seems to be that if the short
name is in scope, the longer name gets filtered out. Adding another
inductive which introduces another "foo1" rule confirms that observation.
inductive foo2 :: "nat ⇒ bool" where
foo1: "foo2 0"
thm foo<Ctrl-B>
... now has "foo.foo1", but not "foo2.foo1".
Could this be changed or configurable? Sometimes, it is preferable to
give the long names, even if the shorter ones are in scope.
Side note: Pressing <Ctrl-B> after "thm foo." (notice the dot) doesn't
open the completion dialog.
Cheers
Lars
Email Gateway (Aug 19 2022 at 15:37):From: Makarius <makarius@sketis.net>
On Thu, 31 Jul 2014, Lars Hupel wrote:
assume this simple inductive definition:
inductive foo :: "nat ⇒ bool" where
foo1: "foo 0"Now, trying the completion:
thm foo<Ctrl-B>
... this gives me "foo.cases", "foo.induct", ... (as expected), and also
"foo1". It doesn't give me "foo.foo1", though.Peter suggested that the general policy seems to be that if the short
name is in scope, the longer name gets filtered out.
This corresponds to certain canonical ways to deal with internal vs.
external names in name spaces. The bahaviour comes out naturally without
further ado, and without rethinking the usual ways.
Could this be changed or configurable?
To do different one needs a clear counter-indication that the default is
not right. Lets say 2-3 convincing application scenarios. Configurable
"modes" are a measure of last resort, when there is no clear uniform
approach anymore.
Side note: Pressing <Ctrl-B> after "thm foo." (notice the dot) doesn't
open the completion dialog.
The dot is a keyword and already complete on its own. If you want to
complete the name fragment "foo." you have to write it in quotes, and it
then gets correctly expanded without quotes.
Makarius
Last updated: Nov 21 2024 at 12:39 UTC