Hi again,
> datatype_new 'a list =
> Nil (defaults un_Cons2: "[]") ("[]")
> | Cons 'a "'a list" (infixr "#" 65)
>
> abbreviation "map ≡ map_list"
> abbreviation "set ≡ set_list"
> abbreviation "list_all2 ≡ rel_list"
> abbreviation "hd ≡ un_Cons1"
> abbreviation "tl ≡ un_Cons2"
this would make sen
Hi all,
many issues have been touched in this thread, but I would like to get
back to the proposals made by Jasmin which IMHO point into the right
direction.
> 1. The squiggles (-: and =:) are easy to get rid of, and we'll kill
> them. This has been discussed before.
OK. No need to discuss this
On Mon, 26 May 2014, Jasmin Christian Blanchette wrote:
Am 26.05.2014 um 12:34 schrieb Lawrence Paulson :
What new users see when they look at the actual definition of lists is
not that important. There are many, many situations where the actual
definition of something is much more complicate
On 26/05/2014 16:13, Jasmin Christian Blanchette wrote:
> Am 26.05.2014 um 12:34 schrieb Lawrence Paulson :
>
>> What new users see when they look at the actual definition of lists is not
>> that important. There are many, many situations where the actual definition
>> of something is much more
Am 26.05.2014 um 12:34 schrieb Lawrence Paulson :
> What new users see when they look at the actual definition of lists is not
> that important. There are many, many situations where the actual definition
> of something is much more complicated than the idealised version that one
> would use fo
On Mon, 26 May 2014, Andrei Popescu wrote:
getSelector isNil for Nil[list]
BTW, camelCaseIsNotUsedInIsabelleSourcesToImproveReadability.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenche
On Mon, 26 May 2014, Jasmin Blanchette wrote:
Am 26.05.2014 um 15:24 schrieb Makarius :
I think you could afford an actual keyword for the "dead" modifier and
use it without colon, like "lazy" in HOLCF/domain. That would
substract "dead" from the normal identifier space, but merely means its
On Mon, 26 May 2014, Andrei Popescu wrote:
Then people suggested that this name is too unspecific and I came up
with "BNF" ("bounded natural functor"), which summarizes the main
components: a natural transformation "set", a cardinal bound, and a
functor.
This more specific name however loses
Am 26.05.2014 um 15:24 schrieb Makarius :
> I think you could afford an actual keyword for the "dead" modifier and use it
> without colon, like "lazy" in HOLCF/domain. That would substract "dead" from
> the normal identifier space, but merely means its very few occurrences on
> AFP/Jinja and A
On Mon, 26 May 2014, Jasmin Blanchette wrote:
Am 26.05.2014 um 13:41 schrieb Dmitriy Traytel :
Yes, we have considered this naming earlier. It was discarded, because
it looks like one is giving the name "dead" to a set function. The same
holds for any other identifier (not only the common one
Am 26.05.2014 um 14:28 schrieb Andrei Popescu :
> I have the following proposal:
>
> (1) Hide all the extra structure from the user if it is not required
> explicitly.
>
> (2) Make parts of this structure visible upon request by "get" commands that
> specify the target datatype and the desired
I have a comment followed by a suggestion.
Three years ago when I introduced the concept of BNF, I initially called it
"enriched type constructor".
Then people suggested that this name is too unspecific and I came up with "BNF"
("bounded natural functor"),
which summarizes the main compon
Am 26.05.2014 um 12:05 schrieb Makarius :
> The observed here problem is different: the type constructor "list" somehow
> ends up in the name space with a "concealed" flag. There might be one or
> more Binding.conceal too many in the BNF sources.
Ah, now I get it. Of course this is entirely ac
Am 26.05.2014 um 12:25 schrieb Makarius :
> On Sun, 25 May 2014, Jasmin Christian Blanchette wrote:
>
>> The "=" as the name for Nil's discriminator deserves an explanation. [...]
>> So I introduced this weird "=" syntax, which suggests that equality is used
>> for discriminating. I am open to
Am 26.05.2014 12:53, schrieb Makarius:
On Mon, 26 May 2014, Dmitriy Traytel wrote:
Just on the squiggles in isolation: if these are rare add-on
options one
could invent long / explicit keywords for them (or Parse.literal
items).
grep gives 371 occurences of "-:" in IsaFoR's development rep
On Mon, 26 May 2014, Dmitriy Traytel wrote:
Just on the squiggles in isolation: if these are rare add-on options one
could invent long / explicit keywords for them (or Parse.literal items).
grep gives 371 occurences of "-:" in IsaFoR's development repository. So
it's not a rare add-on, but
What new users see when they look at the actual definition of lists is not that
important. There are many, many situations where the actual definition of
something is much more complicated than the idealised version that one would
use for teaching. What is necessary is that simple-looking defini
Am 26.05.2014 12:25, schrieb Makarius:
On Sun, 25 May 2014, Jasmin Christian Blanchette wrote:
The "=" as the name for Nil's discriminator deserves an explanation.
[...] So I introduced this weird "=" syntax, which suggests that
equality is used for discriminating. I am open to other suggestio
> Let's distinguish between A = {hd, tl} and B = {map, set, rel}. The constants
> from B are an integral part of the package---they form together with the type
> a BNF. Thus, they will always be "generated". The question is whether they
> are exposed to the user.
Well, they necessarily need to
On Sun, 25 May 2014, Jasmin Christian Blanchette wrote:
The "=" as the name for Nil's discriminator deserves an explanation.
[...] So I introduced this weird "=" syntax, which suggests that
equality is used for discriminating. I am open to other suggestions.
The other funky syntax we have is
Just to be clear on this: the ability to get all of these functions for free is
marvellous! We are now discussion only the syntactic interface to that
marvellous functionality, how much is exposed by default, and in particular in
the defn of list.
Tobias
On 26/05/2014 12:14, Dmitriy Traytel wrote
Am 26.05.2014 11:46, schrieb Tobias Nipkow:
On 26/05/2014 11:07, Jasmin Blanchette wrote:
Am 26.05.2014 um 11:02 schrieb Tobias Nipkow :
The definition of list should look like before.
I don't see how this is an option. This would result in the following duplicate
constants:
map_list
I have no particular stake in this issue, but I would think there was an
option (c) which is to do the *opposite* of what Jasmin said about
bringing the additional constant names etc as close as possible to
wherever they "fit":
datatype_new 'a list =
Nil ("[]")
| Cons 'a "'a list" (infix
On Sun, 25 May 2014, Jasmin Christian Blanchette wrote:
(3) A genuine name space problem: "list" is concealed, and thus cannot
be completed in semantic completion.
I presume you are referring to the fact that
@{const_name Cons} = "List.list.Cons"
@{const_name hd} = "List.list.hd"
@{c
Am 26.05.2014 11:07, schrieb Jasmin Blanchette:
Am 26.05.2014 um 11:02 schrieb Tobias Nipkow :
The definition of list should look like before.
I don't see how this is an option. This would result in the following duplicate
constants:
map_list vs. map
set_list vs. set
rel_list
On 26/05/2014 11:07, Jasmin Blanchette wrote:
> Am 26.05.2014 um 11:02 schrieb Tobias Nipkow :
>
>> The definition of list should look like before.
>
> I don't see how this is an option. This would result in the following
> duplicate constants:
>
> map_list vs. map
> set_list vs. set
Am 26.05.2014 um 11:02 schrieb Tobias Nipkow :
> The definition of list should look like before.
I don't see how this is an option. This would result in the following duplicate
constants:
map_list vs. map
set_list vs. set
rel_list vs. forall_list2
un_Cons1 vs. hd
un_Cons2 vs
The definition of list should look like before.
Tobias
On 26/05/2014 10:59, Jasmin Christian Blanchette wrote:
> Am 26.05.2014 um 10:30 schrieb Tobias Nipkow :
>
>> I can only agree with what Makarius has observed but would go one step
>> further:
>> the new definition of list is truly baroque
Am 26.05.2014 um 10:30 schrieb Tobias Nipkow :
> I can only agree with what Makarius has observed but would go one step
> further:
> the new definition of list is truly baroque and unsuitable for beginners, but
> beginners are bound to look at it. Sometimes languages have to reduce
> complexity
On 26/05/2014 10:30, Tobias Nipkow wrote:
> The three types bool, nat and list should be defined in
> the plain standard manner.
Ignore the bit about bool and nat.
Tobias
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informa
I can only agree with what Makarius has observed but would go one step further:
the new definition of list is truly baroque and unsuitable for beginners, but
beginners are bound to look at it. Sometimes languages have to reduce complexity
to cater for novices. The three types bool, nat and list sho
31 matches
Mail list logo
