On 12/06/2016 18:22, Florian Haftmann wrote:
Thus I would like to understand why we cannot reuse Sup etc in HOLCF
like we do for all the other variants of lattices we have. We would
probably need a suitable type class because at the moment lub is
unrestricted.
For each type class, per type
> Thus I would like to understand why we cannot reuse Sup etc in HOLCF
> like we do for all the other variants of lattices we have. We would
> probably need a suitable type class because at the moment lub is
> unrestricted.
For each type class, per type constructor there is at most *one*
On 11/06/2016 21:26, Florian Haftmann wrote:
For the moment I think bold syntax in the first choice. In the middle
run I would suggest to have a closer look at HOLCF/Porder.thy to see
whether something can be done to integrate it more with the standard
type classes; a least it formalizes a
Hi Makarius,
Am 11.06.2016 um 00:13 schrieb Makarius:
> On 10/03/16 11:19, Makarius wrote:
>> On Thu, 10 Mar 2016, Johannes Hölzl wrote:
>>
>>> Alternatively: Would a lattice_syntax locale work nowadays? I remember
>>> I tried it once and for some reason it didn't work. Either notations
>>>
On 10/03/16 11:19, Makarius wrote:
> On Thu, 10 Mar 2016, Johannes Hölzl wrote:
>
>> Alternatively: Would a lattice_syntax locale work nowadays? I remember
>> I tried it once and for some reason it didn't work. Either notations
>> aren't supported in locales or they are exported after the context
On 10/03/2016 11:00, Florian Haftmann wrote:
Hi all,
traditionally, syntax for lattice operations (⊓ ⊔ ⊥ ⊤ etc.) has been
kept in a separate library theory, to allow use of that quite generic
notation for unforeseen applications.
Meanwhile however all those operations to which
On Thu, 10 Mar 2016, Johannes Hölzl wrote:
Alternatively: Would a lattice_syntax locale work nowadays? I remember I
tried it once and for some reason it didn't work. Either notations
aren't supported in locales or they are exported after the context
-block.
The concept of 'bundle' was
> What would be the objective of this change?
Mainly to get rid of those brittle (no_)notation declarations scattered
over various theories. Organizing syntax through library theories does
not quite work out.
Florian
>
>> On 10 Mar 2016, at 10:00, Florian Haftmann
>>
What would be the objective of this change?
Larry
> On 10 Mar 2016, at 10:00, Florian Haftmann
> wrote:
>
> Hi all,
>
> traditionally, syntax for lattice operations (⊓ ⊔ ⊥ ⊤ etc.) has been
> kept in a separate library theory, to allow
Am Donnerstag, den 10.03.2016, 11:00 +0100 schrieb Florian Haftmann:
> Hi all,
>
>
> traditionally, syntax for lattice operations (⊓ ⊔ ⊥ ⊤ etc.) has been
> kept in a separate library theory, to allow use of that quite generic
> notation for unforeseen applications.
>
> Meanwhile
Hi all,
traditionally, syntax for lattice operations (⊓ ⊔ ⊥ ⊤ etc.) has been
kept in a separate library theory, to allow use of that quite generic
notation for unforeseen applications.
Meanwhile however all those operations to which that syntax is attached
to are members of
11 matches
Mail list logo