Matteo Manighetti cde6ba24c9 Merge remote-tracking branch 'why3-inria/master' into why3-devel

2024-02-20 11:14:13 +01:00

..

mach

reinforce pre-conditions of safe machine floats operations

2023-09-18 17:42:25 +02:00

algebra.mlw

add a meta to mark a symbol as never removed by remove_unused*

2023-06-15 15:18:48 +00:00

array.mlw

Separate logical and program function Array.make

2021-01-15 12:39:37 +01:00

bag.mlw

stdlib: added bag intersection

2020-12-05 11:01:24 +01:00

bintree.mlw

stdlib, examples: remove redundant "import"

2018-06-15 16:45:58 +02:00

bool.mlw

stdlib: rename *.why to *.mlw, use "module" instead of "theory"

2017-12-22 15:46:12 +01:00

bv.mlw

Facilitate proof of arithmetic on bitvectors by Alt-Ergo

2024-02-20 11:10:10 +01:00

byte_string.mlw

stdlib: proper postcondition for (=) on bounded integers

2023-06-17 00:16:27 +00:00

cursor.mlw

Add modules in the stdlibdoc

2019-06-05 18:57:02 +02:00

debug.mlw

reflection printfs and add_limbs example

2018-01-16 11:15:11 +01:00

exn.mlw

Add modules in the stdlibdoc

2019-06-05 18:57:02 +02:00

floating_point.mlw

Generalization of check_unused_vars to logic and program decl

2019-08-20 15:48:44 +02:00

fmap.mlw

Improve documentation of standard library.

2021-09-21 18:00:14 +02:00

for_drivers.mlw

Revert "Simplify euclidean to computer division"

2023-10-19 12:12:59 +02:00

function.mlw

Add modules in the stdlibdoc

2019-06-05 18:57:02 +02:00

graph.mlw

stdlib, examples: remove redundant "import"

2018-06-15 16:45:58 +02:00

hashtbl.mlw

Improve documentation of standard library.

2021-09-21 18:00:14 +02:00

ieee_float.mlw

Merge remote-tracking branch 'why3-inria/master' into merge_inria_why3_1_7_0

2024-01-11 18:00:47 +01:00

int.mlw

Merge remote-tracking branch 'why3-inria/master' into merge_inria_why3_1_7_0

2024-01-11 18:00:47 +01:00

io.mlw

Document module "io" (fix #554).

2021-09-23 15:11:55 +02:00

list.mlw

stdlib list.mlw: Add contract to Quant.{for_all, for_some, mem}

2019-10-01 15:23:25 +02:00

map.mlw

no more theory sum.Sum

2020-02-12 10:30:25 +01:00

matrix.mlw

Matrix: add the pure "update" function for applicative updates

2018-07-02 17:15:42 +02:00

microc.mlw

Dexpr: emit a warning for spurious olds in val contracts

2021-03-12 20:56:41 +01:00

number.mlw

stdlib, examples: remove redundant "import"

2018-06-15 16:45:58 +02:00

ocaml.mlw

stdlib: ocaml exception Invalid_argument moved to ocaml.Exceptions

2020-06-22 18:38:26 +02:00

option.mlw

stdlib: added a new theory option.Map

2020-08-25 14:53:07 +02:00

pigeon.mlw

Improve documentation of standard library.

2021-09-21 18:00:14 +02:00

pqueue.mlw

Add safe_peek and safe_pop in all pqueue modules

2019-07-03 16:11:41 +02:00

python.mlw

micro-Python: add_list can be used in logic

2022-11-14 14:58:24 +01:00

queue.mlw

Improve documentation of standard library.

2021-09-21 18:00:14 +02:00

random.mlw

stdlib, examples: remove redundant "import"

2018-06-15 16:45:58 +02:00

real.mlw

add a meta to mark a symbol as never removed by remove_unused*

2023-06-15 15:18:48 +00:00

ref.mlw

Improve documentation of standard library.

2021-09-21 18:00:14 +02:00

regexp.mlw

Add modules in the stdlibdoc

2019-06-05 18:57:02 +02:00

relations.mlw

Changed the unsecure trusted_wf attribute mechanism into a more secure one

2023-02-22 13:50:29 +00:00

seq.mlw

Fix occurrences of "occurences".

2023-11-23 19:04:11 +01:00

set.mlw

cardinal of finite products

2021-06-27 13:21:36 +02:00

stack.mlw

library: {Stack,Queue}.length now return a Peano.t

2018-10-26 15:47:03 +02:00

string.mlw

Fix occurrences of "occurences".

2023-11-23 19:04:11 +01:00

tptp.mlw

stdlib, examples: remove redundant "import"

2018-06-15 16:45:58 +02:00

tree.mlw

Add modules in the stdlibdoc

2019-06-05 18:57:02 +02:00

ufloat.mlw

Forward propagation of rounding errors

2024-01-18 10:31:14 +00:00

witness.mlw

library: two versions of witness

2018-06-17 11:09:22 +02:00