Jean-Christophe Filliatre
aedb2eb09d
examples: variant of Kadane's algorithm
...
we look for the maximal product instead of the maximal sum
(this commit also applies auto-dereference everywhere in the file)
2024-02-11 19:11:47 +01:00
Andrei Paskevich
eae547d95f
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
Andrei Paskevich
7b0929a761
WhyML: "use/clone T" imports by default (in absence of "as")
...
For the previous behaviour (no import), write "use/clone T as T".
This shortens the most used "use/clone import" to simply "use/clone".
2018-06-15 16:45:58 +02:00
Jean-Christophe Filliatre
4898a45de1
mach.array.Array63 now uses a sequence as a model
...
instead of a function of type int->'a
a coercion is declared from arrays to sequences, so that notation a[i]
in the logic now refers to the sequence operation
small caveat: you have to open module seq.Seq to be able to use this
notation
2018-05-14 15:59:35 +02:00
Guillaume Melquiond
9e92f8203f
Change label syntax from "foo" to [@foo].
...
The feature is not yet fully implemented (e.g. escape characters).
2018-01-12 18:05:43 +01:00
Jean-Christophe Filliatre
9356fe25e0
updated examples using cool new features
2017-06-06 14:02:05 +02:00
Jean-Christophe Filliatre
c600769053
Kadane's algorithm with bounded integers
2017-06-06 11:02:14 +02:00
Guillaume Melquiond
96addbf6b3
Reduce amount of "use export" in the standard library.
2014-08-21 17:52:20 +02:00
Andrei Paskevich
d7eef7317f
add a variation of Kadane's algorithm to examples/maximum_subarray
2013-10-19 21:48:02 +02:00
Jean-Christophe Filliatre
6e5d6e58bb
maximum subarray: doc and credits
2013-09-25 17:27:41 +02:00
Guillaume Melquiond
496ca632e6
Fix program and finish proof of maximum_subarray.
2013-09-25 16:55:42 +02:00
