> On 28.07.2016, at 10:33, Peter Lammich wrote:
>
>>> How about
>>>
>>> definition add_mset :: "'a ⇒ 'a multiset ⇒ 'a multiset" ("add#") where
>>> "add# x M = {#x#} + M"
>
> This, however, may produce confusion with multiset union, which is an
> instance of the plus type
On 28/07/2016 10:33, Peter Lammich wrote:
On Do, 2016-07-28 at 10:21 +0200, Jasmin Blanchette wrote:
Tobias wrote:
How about
definition add_mset :: "'a ⇒ 'a multiset ⇒ 'a multiset" ("add#") where
"add# x M = {#x#} + M"
This, however, may produce confusion with multiset union, which is an
I've been using multisets quite a bit myself lately. add# and add1# both
sound all right to me.
I would also like to point out that for some reason, intersection and
union are #∪ and #∩, whereas all other multiset operations seem to have
the # at the end (e.g. ⊆#). Unless there is some deeper
On 27/07/2016 11:39, Jasmin Blanchette wrote:
Tobias wrote:
Did we ever discuss the naming issue? "insert_mset" would be the canonical
name, but it would make larger expressions hard to read.
I'm not so sure "insert_mset" would be the right name. Its set-based
terminology might suggest a
On Do, 2016-07-28 at 10:21 +0200, Jasmin Blanchette wrote:
> Tobias wrote:
>
> > How about
> >
> > definition add_mset :: "'a ⇒ 'a multiset ⇒ 'a multiset" ("add#") where
> > "add# x M = {#x#} + M"
This, however, may produce confusion with multiset union, which is an
instance of the plus type
Tobias wrote:
> How about
>
> definition add_mset :: "'a ⇒ 'a multiset ⇒ 'a multiset" ("add#") where
> "add# x M = {#x#} + M"
Lovely!
Jasmin
___
isabelle-dev mailing list
isabelle-...@in.tum.de
>> Tobias wrote:
>>
>>> How about
>>>
>>> definition add_mset :: "'a ⇒ 'a multiset ⇒ 'a multiset" ("add#") where
>>> "add# x M = {#x#} + M"
>
> This, however, may produce confusion with multiset union, which is an
> instance of the plus type classes, i.e., occupying the name
> plus_multiset.
To
Just an aside: concerning »insert« and »add«, infix syntax would be
desirable, e.g.
a `insert` X
a `add` M
similar to
Y \union Y
N + M
which would yield much more readable propositions, esp. wrt. associativity:
a `insert` b `insert` X = {a, b} \union X
> I would also like to point out that for some reason, intersection and union
> are #∪ and #∩, whereas all other multiset operations seem to have the # at
> the end (e.g. ⊆#). Unless there is some deeper reason for this, I suggest we
> change it.
Good point. Indeed, I first wrote ∪# in
Yes, that might be a good idea.
On 27/07/16 11:24, Tobias Nipkow wrote:
Naming: can't we drop "is_"?
Tobias
On 27/07/2016 10:46, Manuel Eberl wrote:
*** HOL ***
* Number_Theory: algebraic foundation for primes: Introduction of
predicates "is_prime", "irreducible", a "prime_factorization"
With Isabelle/e506baad44fa we are on jdk-8u102, which is a recent update
by Oracle with a lot of changes.
See also
http://www.oracle.com/technetwork/java/javase/8u102-relnotes-3021767.html
http://www.oracle.com/technetwork/java/javase/2col/8u102-bugfixes-3021768.html
Occording to my
11 matches
Mail list logo