**Mário Pereira**
(596d15ae)
*
at
04 Feb 15:37
*

**Mário Pereira**
(596d15ae)
*
at
04 Feb 14:48
*

Use of `:file:`

and `:option:`

directives

*
... and
1 more commit
*

This is a draft for the documentation of functors extraction.

**Mário Pereira**
(ca55f5e3)
*
at
04 Feb 14:16
*

Typo.

**Mário Pereira**
(4e746f3f)
*
at
03 Feb 23:00
*

Typo.

This is a draft for the documentation of functors extraction.

**Mário Pereira**
(58dd7e4c)
*
at
03 Feb 22:57
*

Documentation of functors extraction.

That is correct :) #493 is only about automatically introduce a `val ghost`

function, with the same contract as the lemma you wish to instantiate.

But are you proposing we accept `module J : I ... end`

even when `I`

and `J`

share defined symbols (for instance, by lifting such definitions into a separated module as you suggest), or that this should always fail?

Honestly, I am in favor of failing. In such cases, the `Cannot instantiate a defined symbol`

error message is quite clear, and the user will easily understand what she is doing. She can then go and change its definitions into axioms, which she will immediately have to prove because of the cloning.

Okay, I will make the necessary changes.

I am definitely not sure about this change. If we print a tuple using the value of `paren`

we get the behavior reported in #509 (closed). I do believe we should always print tuples in algebraic constructors with surrounding parentheses. However, for the tuple elements, I am not sure what is the correct value that we should use for `paren`

. On one hand, always using `~paren:true`

leads to some undesired results, such as

` type t = A of ((int) * (bool)) * string`

On the other hand, it feels a bit odd to propagate the value of `paren`

to the elements in the tuple, while simply ignoring it for the tuple itself.

I guess we are definitely not used to have algebraic constructors with tuple arguments in WhyML :)

It does support nullary constants, cf http://why3.lri.fr/stdlib/mach.peano.html (here `zero`

and `one`

are 0-arity constants).

However, according to the VSTTE'15 paper (https://hal.inria.fr/hal-01162661v2/document, page 8), one-time `zero`

and `one`

cannot be constants since they must return a fresh one-time integer each time.
@filliatr @paskevyc

This fixes #509

**Mário Pereira**
(baafa99d)
*
at
13 Nov 14:40
*

Fixed extraction of parentheses around inlined tuples.

**Mário Pereira**
(a2bfb09f)
*
at
13 Nov 14:15
*

Fixed extraction of one-time constants `zero`

and `one`

.

Will this approach also take `function`

and `predicate`

into account? If that is the case, what is the chosen behavior when both the interface and the implementation provide definitions for the same symbol? Consider for instance Skew Heaps, in particular the definition of predicates `mem`

and `is_minimum`

: http://toccata.lri.fr/gallery/skew_heaps.en.html

**Mário Pereira**
(dccef8ab)
*
at
10 Sep 17:13
*

No more `let empty () = ...`

in examples.

I think this is due to the use of the `=`

operation in a program routine.

**Mário Pereira**
(1349b793)
*
at
21 Jul 18:04
*

mlcfg: new example arith.Fact