On 23/12/2010, at 3:46 AM, Claude Marche wrote:
>
>
> We are happy to announce the first public release of Why3, also known
> as the Why platform next generation. It is a new project, independent
> from Why versions 2.xx.
> 3) Source code organized as a library with a documented API,
> to allo
On Tue, 2007-10-02 at 20:37 +1000, skaller wrote:
> On Mon, 2007-10-01 at 22:34 -0700, Erick Tryzelaar wrote:
> /
> instance[T,U] Str[T * U] {
> fun str (x:T, y:U)=> str x + ", " + str y;
> }
> instance Str[unit] {
> fun str() => "";
> }
>
> println
On Tue, 2007-10-02 at 09:10 -0700, Erick Tryzelaar wrote:
> On 10/2/07, skaller <[EMAIL PROTECTED]> wrote:
> > open Foo;
> >
> > doesn't work.
>
> Actually, It did work for me. I also used "open[T] Foo[T]", which
> worked as well.
Hmm .. I wonder why. Perhaps it automatically quantifies
On 10/2/07, skaller <[EMAIL PROTECTED]> wrote:
> On Mon, 2007-10-01 at 22:34 -0700, Erick Tryzelaar wrote:
> > On 10/1/07, skaller <[EMAIL PROTECTED]> wrote:
>
> > I didn't know that that's all you needed to do. Now I think I
> > understand why my "open instance" was wrong. So, since "typeclass
> >
On Mon, 2007-10-01 at 22:34 -0700, Erick Tryzelaar wrote:
> On 10/1/07, skaller <[EMAIL PROTECTED]> wrote:
> I didn't know that that's all you needed to do. Now I think I
> understand why my "open instance" was wrong. So, since "typeclass
> Foo[T] { ... } open Foo;" works, should we add support fo
On Mon, 2007-10-01 at 22:34 -0700, Erick Tryzelaar wrote:
> On 10/1/07, skaller <[EMAIL PROTECTED]> wrote:
> Yes I'm aware of that problem and it's great to hear you might have a
> solution to it.
Well, this works now:
/
instance[T,U] Str[T * U] {
f
On 10/1/07, skaller <[EMAIL PROTECTED]> wrote:
> BTW: probably more important, as pointer out by the last deserter ..
> typeclasses for I/O. There's only so much you can do calculating
> 2 + 40 and printing to the console.
I'm working my way there. I'm still trying to conceptualize how to
talk to
On 10/1/07, skaller <[EMAIL PROTECTED]> wrote:
> My turn next .. been reading the Ruby docs .. so I can understand
> your weird
>
> (1,2,3).foreach { |i| print i }
>
> stuff. Well, the doc explains this isn't what I thought it was:
> in fact, the LHS and RHS are coroutines.
>
> So actually,
On Mon, 2007-10-01 at 17:58 -0700, Erick Tryzelaar wrote:
> What do you think about starting to migrate
> the instances into the modules for things like list, varray, and etc?
BTW: probably more important, as pointer out by the last deserter ..
typeclasses for I/O. There's only so much you can d
On Mon, 2007-10-01 at 17:58 -0700, Erick Tryzelaar wrote:
> On 10/1/07, skaller <[EMAIL PROTECTED]> wrote:
> /me goes back to misunderstanding things :)
My turn next .. been reading the Ruby docs .. so I can understand
your weird
(1,2,3).foreach { |i| print i }
stuff. Well, the doc exp
On 10/1/07, skaller <[EMAIL PROTECTED]> wrote:
> Anyhow, I think (LOL!) it works like this: here is println:
>
> proc println[T with Str[T]] (x:T) {
> fprint (cout, str x);
> endl cout;
> };
>
>
> Now, println itself is 'opening Str[T]' for ALL T.
> For this to work, Str must be
On Mon, 2007-10-01 at 15:30 -0700, Erick Tryzelaar wrote:
> I noticed that with the list instance of Str doesn't need to open the
> instance to have it be usable, as shown in this example:
>
> val x = List::list (1, 2, 3);
> println $ x;
>
> (btw, I love not having to import flx.flxh :) )
>
> Di
With only one exception, failure, Felix now produces
*.why files for every compilation that pass thru why
syntax checks. The exception is a stupid test case:
test/regress/rt-1.01.26-0
axiom poly[t] ( sym:t * t -> t, eq:t * t-> bool, x:t, y:t):
sym(x,y) == sym(y,x)
;
which generates th
13 matches
Mail list logo
