Hi Andreas,
The failure happens while reading the locale expression, which is a
sequence of locale instances:
A s + B t + C u + ...
When reading the locale expression, we aim at achieving two conflicting goals:
- Type inference over the entire expression
- Syntax declarations of an
Hi,
I came across a situation where the order of sublocale declarations
makes a difference in the theory development, which in this case is not
clear to me. Can anyone please clarify the following behaviour within
the simplified case below? Is the behaviour due to purely technical
reasons or
Hi Amine,
the error message in the second case is only delayed: You get it, once
you open the AB context again (context AB begin). In the first case, it
shows up immediately, because the sublocale command already constructs
the context AB enriched with B.
Best,
Andreas
On 01/31/2013 12:48
Thanks Andreas. Does this mean that this sublocale scenario is
prohibited? And if so, is it due to technical reasons or is there a
fundamental problem here?
Amine.
On 01/31/2013 02:04 PM, Andreas Lochbihler wrote:
Hi Amine,
the error message in the second case is only delayed: You get it,
Hi Amine,
let's look at what happens:
A defines the constant local.fpower as A.fpower f
AB inherits it from A, i.e., we have local.fpower == A.fpower f (1)
B A d g produces local.fpower == A.fpower (d g)
AB B d f inherits this as local.fpower == A.fpower (d (d f)) (2)
As the locale
Hi Andreas, T
his is of great help. Thank you, especially for the rewriting hint. I
was thinking modulo that equation.
This solves my concrete problem, but I am still intrigued by the
behaviour and its reasons.
Amine.
On 01/31/2013 03:21 PM, Andreas Lochbihler wrote:
Hi Amine,
let's
