Email Gateway (Aug 18 2022 at 13:42): Email Gateway (Aug 18 2022 at 13:42):From: Christian Sternagel <christian.sternagel@uibk.ac.at>
I think a related issue is that it is not possible to use the identifier
'all', e.g., I wanted to have the list function
primrec all :: "('a => bool) => 'a list => bool"
where "all p [] = True"
| "all p (x#xs) = (p x \<and> all p xs)"
The definition ran through... however, at some later point I tried to
use a formula of the form "!!x. ?P x" and there I got a type error.
Would this problem also be solved if the internal constant for `!!'
would be qualified... or is it a different problem?
cheers
chris
P.S.: is there some workaround that lets me use the function name 'all'?
Email Gateway (Aug 18 2022 at 13:42):From: Makarius <makarius@sketis.net>
The Pure quantifier is called "all" internally -- this is a global name
with "non-authentic" syntax. This means there is no way to use that base
name in some user theory -- neither name space accesses nor notation can
be modified later without breakdown.
While we have worked hard to reduce the number of (historical) global
constants like this for HOL (and the process is not really finished yet),
this is even harder for Pure. So global names are likely to persist there
for > 10 more years.
Makarius
Last updated: May 03 2024 at 04:19 UTC