> I think there is a formal difference here that is beyond "Isar" vs. "ML":
>
> a) If function calls inductive, then it is exclusively interested in
> getting an inhabitant of a specification in the auxiliary context (which
> I nowadays prefer to call the "package context"). Its interpretation in
Brian Huffman wrote:
*My* first idea was that "typedef" didn't need to be defining a set
constant at all.
(I would appreciate if we could keep this discussion focused. To discuss
typedef, please start a new thread.)
Makarius wrote:
When we speak about "users" of packages it covers both ML a
What you specify is a type constraint for the main body of the
specification text. There can be a mismatch of what the system
infers as most general type and what you've had in mind. There can
be also surprises due to type abbreviations.
Which situation did you have exactly?
I don't hav
On Thu, 2 Dec 2010, Brian Huffman wrote:
If the default behavior of the "typedef" command was to work like
"typedef (open)" (and I think it ought to be), then there would have
been no problem
There would have been no problem in this example, but the problem still
exists in general, and had b
On Thu, Dec 2, 2010 at 11:26 AM, Makarius wrote:
> Back to history: in 2005 Brian had a paper on TPHOLs with a footnote about
> an unexpected crash of the typedef package due to hidden polymorphism in the
> set involved, not the type.
It was a simple error message, not a "crash".
> What I did th
On Thu, 2 Dec 2010, John Matthews wrote:
As another user data point, a few months back I ran into this same issue
of the type I specified not being the type Isabelle gave me back. It was
pretty confusing at the time and it took me a while to figure out what
was going on.
Sorry, I don't quite
On Thu, 2 Dec 2010, Tobias Nipkow wrote:
The interface is a red herring. The discussion is on the concept at the
user level.
Here is again a current snapshot with everything built and bundled
http://www.lri.fr/~wenzel/Isar2010-Orsay/download.html
The new interaction model seriously changes
As another user data point, a few months back I ran into this same
issue of the type I specified not being the type Isabelle gave me
back. It was pretty confusing at the time and it took me a while to
figure out what was going on.
-john
On Dec 2, 2010, at 11:26 AM, Makarius wrote:
On Thu
On Thu, 2 Dec 2010, Alexander Krauss wrote:
I'll have a look at the code and see if packages can reject this from
the user, while still being composable. This applies to all packages.
In fact I've made this error already in 2005, and it was Alex himself who
convinced me more recently that pac
Makarius wrote:
Maybe Florian (and Alex) can post again the concrete examples they were
mentioning to me 1 or 2 years ago.
The original problem was that the function package sometimes issues an
inductive definition with hidden polymorphism whenever there are type
variables in the function typ
The interface is a red herring. The discussion is on the concept at the
user level. If it is not generally useful but only in very arcane
situations, it should not happen implicitly, but the arcane situations
should be required to state the dependence explicitly. We have this
explicit over implicit
On Thu, Dec 2, 2010 at 8:42 AM, Makarius wrote:
> Right now there is already a clear warning -- which Proof General happens to
> show in a hardly visible way, but that is just one of many problems of Proof
> General. In Isabelle/jEdit the warning is hard to miss. I will check again
> about the ot
On Thu, 2 Dec 2010, Brian Huffman wrote:
But if we had something like a "fixes" clause for types, it would look
nicer and indicate the intention unambiguously, making a warning message
unnecessary:
locale count = fixes_type 'a assumes ex_inj: "EX f::'a => nat. inj f"
This would be a substan
On Thu, 2 Dec 2010, Tobias Nipkow wrote:
Florian explained to me that for the function package this new behaviour
is an improvement, but that does not mean that unsuspecting users should
be subjected to it.
Maybe Florian (and Alex) can post again the concrete examples they were
mentioning to
Thank you Brian, that seems to sum up the situation rather nicely. We
should return to the old behaviour at the top level where definitions
did not acquire additional parameters. Florian explained to me that for
the function package this new behaviour is an improvement, but that does
not mean that
I agree!
Larry
On 2 Dec 2010, at 14:44, Brian Huffman wrote:
> Besides these two very specific cases, I think it would be best to
> reject definitions with extra type variables on the right-hand side.
___
isabelle-dev mailing list
isabelle-...@in.tum.d
On Wed, Dec 1, 2010 at 11:50 PM, Tobias Nipkow wrote:
> Is the following behaviour really a good idea and useful?
>
> inductive P :: "nat => bool" where
> "P(suc n)"
>
> is accepted but defines
>
> P :: "'a itself => nat => bool"
>
> It does kind of warn me by saying
>
> ### Additional type variab
Is the following behaviour really a good idea and useful?
inductive P :: "nat => bool" where
"P(suc n)"
is accepted but defines
P :: "'a itself => nat => bool"
It does kind of warn me by saying
### Additional type variable(s) in specification of P: 'a
but if you miss that warning, you will be
18 matches
Mail list logo
