ada/why3
0
0
Fork 0
mirror of https://github.com/AdaCore/why3.git synced 2026-02-12 12:34:55 -08:00
Code Issues Packages Projects Releases Wiki Activity
Files
24-sustained
why3/examples
History
Matteo Manighetti c510b9304c From Inria Why3: new meta remove-constant
2023-06-08 09:59:02 +02:00
..
add_list
Initial bulk upgrade of z3
2023-04-13 09:43:18 +00:00
add_list_vc_sp
fix sessions
2022-07-07 15:49:23 +02:00
algo63
update sessions, including prover upgrade Alt-Ergo 2.0.0 -> 2.1.0 when possible
2023-04-05 13:48:22 +02:00
algo64
update sessions, including prover upgrade Alt-Ergo 2.0.0 -> 2.1.0 when possible
2023-04-05 13:48:22 +02:00
algo65
update sessions, including prover upgrade Alt-Ergo 2.0.0 -> 2.1.0 when possible
2023-04-05 13:48:22 +02:00
all_distinct
update sessions, including prover upgrade Alt-Ergo 2.0.0 -> 2.1.0 when possible
2023-04-05 13:48:22 +02:00
amortization
fix sessions
2022-07-07 15:49:23 +02:00
arm
update sessions, including prover upgrade Alt-Ergo 2.0.0 -> 2.1.0 when possible
2023-04-05 13:48:22 +02:00
array_most_frequent
Initial bulk upgrade of z3
2023-04-13 09:43:18 +00:00
assigning_meanings_to_programs
update sessions, including prover upgrade Alt-Ergo 2.0.0 -> 2.1.0 when possible
2023-04-05 13:48:22 +02:00
avl
separate transformations for intros, dequant, and remove_unused
2023-04-25 12:20:08 +00:00
bag
Initial bulk upgrade of z3
2023-04-13 09:43:18 +00:00
balance
Initial bulk upgrade of z3
2023-04-13 09:43:18 +00:00
bellman_ford
fix sessions
2022-07-07 15:49:23 +02:00
bignum
Initial bulk upgrade of z3
2023-04-13 09:43:18 +00:00
binary_multiplication
update sessions, including prover upgrade Alt-Ergo 2.0.0 -> 2.1.0 when possible
2023-04-05 13:48:22 +02:00
binary_search
Initial bulk upgrade of z3
2023-04-13 09:43:18 +00:00
binary_search_vc_sp
Add "remove_unused:dependency" to int.ComputerDivision
2022-09-21 20:15:46 +00:00
binary_sort
Add "remove_unused:dependency" to int.ComputerDivision
2022-09-21 20:15:46 +00:00
binary_sqrt
separate transformations for intros, dequant, and remove_unused
2023-04-25 12:20:08 +00:00
binomial
separate transformations for intros, dequant, and remove_unused
2023-04-25 12:20:08 +00:00
binomial_heap
Initial bulk upgrade of z3
2023-04-13 09:43:18 +00:00
bitcount
Initial bulk upgrade of z3
2023-04-13 09:43:18 +00:00
bitvector_examples
update sessions, including prover upgrade Alt-Ergo 2.0.0 -> 2.1.0 when possible
2023-04-05 13:48:22 +02:00
bitvectors
separate transformations for intros, dequant, and remove_unused
2023-04-25 12:20:08 +00:00
bitwalker
Initial bulk upgrade of z3
2023-04-13 09:43:18 +00:00
braun_trees
separate transformations for intros, dequant, and remove_unused
2023-04-25 12:20:08 +00:00
bresenham
update sessions, including prover upgrade Alt-Ergo 2.0.0 -> 2.1.0 when possible
2023-04-05 13:48:22 +02:00
bts
From Inria Why3: new meta remove-constant
2023-06-08 09:59:02 +02:00
bubble_sort
update sessions, including prover upgrade Alt-Ergo 2.0.0 -> 2.1.0 when possible
2023-04-05 13:48:22 +02:00
c_cursor
separate transformations for intros, dequant, and remove_unused
2023-04-25 12:20:08 +00:00
check-builtin
Initial bulk upgrade of z3
2023-04-13 09:43:18 +00:00
checking_a_large_routine
examples: variant of Turing's factorial
2022-08-26 11:27:04 +02:00
coincidence_count
separate transformations for intros, dequant, and remove_unused
2023-04-25 12:20:08 +00:00
coincidence_count_list
separate transformations for intros, dequant, and remove_unused
2023-04-25 12:20:08 +00:00
conjugate
update sessions, including prover upgrade Alt-Ergo 2.0.0 -> 2.1.0 when possible
2023-04-05 13:48:22 +02:00
counting_sort
Initial bulk upgrade of z3
2023-04-13 09:43:18 +00:00
cubic_root
update sessions, including prover upgrade Alt-Ergo 2.0.0 -> 2.1.0 when possible
2023-04-05 13:48:22 +02:00
cursor_examples
Initial bulk upgrade of z3
2023-04-13 09:43:18 +00:00
decrease1
Initial bulk upgrade of z3
2023-04-13 09:43:18 +00:00
defunctionalization
Initial bulk upgrade of z3
2023-04-13 09:43:18 +00:00
dfa_example
separate transformations for intros, dequant, and remove_unused
2023-04-25 12:20:08 +00:00
dfs
Initial bulk upgrade of z3
2023-04-13 09:43:18 +00:00
dijkstra
Initial bulk upgrade of z3
2023-04-13 09:43:18 +00:00
disamb
fix sessions
2022-07-07 15:49:23 +02:00
division
update sessions, including prover upgrade Alt-Ergo 2.0.0 -> 2.1.0 when possible
2023-04-05 13:48:22 +02:00
doc_examples
…
double_wp
separate transformations for intros, dequant, and remove_unused
2023-04-25 12:20:08 +00:00
dyck
update sessions, including prover upgrade Alt-Ergo 2.0.0 -> 2.1.0 when possible
2023-04-05 13:48:22 +02:00
edit_distance
upgrade proofs with Z3 4.6.0 to 4.7.1
2023-04-07 09:37:36 +00:00
equality_up_to_spaces
separate transformations for intros, dequant, and remove_unused
2023-04-25 12:20:08 +00:00
esterel
Initial bulk upgrade of z3
2023-04-13 09:43:18 +00:00
euler001
fix sessions
2023-04-09 18:33:02 +02:00
euler002
Initial bulk upgrade of z3
2023-04-13 09:43:18 +00:00
euler011
separate transformations for intros, dequant, and remove_unused
2023-04-25 12:20:08 +00:00
euler_sieve
separate transformations for intros, dequant, and remove_unused
2023-04-25 12:20:08 +00:00
ewd673
update sessions, including prover upgrade Alt-Ergo 2.0.0 -> 2.1.0 when possible
2023-04-05 13:48:22 +02:00
f_puzzle
separate transformations for intros, dequant, and remove_unused
2023-04-25 12:20:08 +00:00
fact
update sessions, including prover upgrade Alt-Ergo 2.0.0 -> 2.1.0 when possible
2023-04-05 13:48:22 +02:00
fact_vc_sp
fix sessions
2022-07-07 15:49:23 +02:00
fenwick
Add "remove_unused:dependency" to int.ComputerDivision
2022-09-21 20:15:46 +00:00
fib_memo
update sessions, including prover upgrade Alt-Ergo 2.0.0 -> 2.1.0 when possible
2023-04-05 13:48:22 +02:00
fibonacci
separate transformations for intros, dequant, and remove_unused
2023-04-25 12:20:08 +00:00
fill
update sessions, including prover upgrade Alt-Ergo 2.0.0 -> 2.1.0 when possible
2023-04-05 13:48:22 +02:00
find
update sessions, including prover upgrade Alt-Ergo 2.0.0 -> 2.1.0 when possible
2023-04-05 13:48:22 +02:00
finger_trees
update sessions, including prover upgrade Alt-Ergo 2.0.0 -> 2.1.0 when possible
2023-04-05 13:48:22 +02:00
finite_tarski
update sessions, including prover upgrade Alt-Ergo 2.0.0 -> 2.1.0 when possible
2023-04-05 13:48:22 +02:00
flag
update sessions, including prover upgrade Alt-Ergo 2.0.0 -> 2.1.0 when possible
2023-04-05 13:48:22 +02:00
flag2
fix sessions
2022-07-07 15:49:23 +02:00
flexible_arrays
separate transformations for intros, dequant, and remove_unused
2023-04-25 12:20:08 +00:00
foveoos11_challenge1
update sessions, including prover upgrade Alt-Ergo 2.0.0 -> 2.1.0 when possible
2023-04-05 13:48:22 +02:00
foveoos11_challenge2
update sessions, including prover upgrade Alt-Ergo 2.0.0 -> 2.1.0 when possible
2023-04-05 13:48:22 +02:00
foveoos11_challenge3
separate transformations for intros, dequant, and remove_unused
2023-04-25 12:20:08 +00:00
foveoos11-cm
Initial bulk upgrade of z3
2023-04-13 09:43:18 +00:00
gcd
separate transformations for intros, dequant, and remove_unused
2023-04-25 12:20:08 +00:00
gcd_bezout
Add "remove_unused:dependency" to int.ComputerDivision
2022-09-21 20:15:46 +00:00
gcd_bezout_vc_sp
update sessions, including prover upgrade Alt-Ergo 2.0.0 -> 2.1.0 when possible
2023-04-05 13:48:22 +02:00
gcd_vc_sp
separate transformations for intros, dequant, and remove_unused
2023-04-25 12:20:08 +00:00
generate_all_trees
update sessions, including prover upgrade Alt-Ergo 2.0.0 -> 2.1.0 when possible
2023-04-05 13:48:22 +02:00
gnome_sort
fix sessions
2023-04-09 18:33:02 +02:00
hackers-delight
Initial bulk upgrade of z3
2023-04-13 09:43:18 +00:00
hashtbl_impl
separate transformations for intros, dequant, and remove_unused
2023-04-25 12:20:08 +00:00
hillel_challenge
separate transformations for intros, dequant, and remove_unused
2023-04-25 12:20:08 +00:00
huffman_with_two_queues
separate transformations for intros, dequant, and remove_unused
2023-04-25 12:20:08 +00:00
i_cant_believe_it_can_sort
Add more meta for explicit dependencies in the bitvector library
2022-09-22 13:40:12 +00:00
induction
Initial bulk upgrade of z3
2023-04-13 09:43:18 +00:00
infinity_of_primes
Add "remove_unused:dependency" to int.ComputerDivision
2022-09-21 20:15:46 +00:00
insertion_sort
separate transformations for intros, dequant, and remove_unused
2023-04-25 12:20:08 +00:00
insertion_sort_list
update sessions, including prover upgrade Alt-Ergo 2.0.0 -> 2.1.0 when possible
2023-04-05 13:48:22 +02:00
insertion_sort_naive
fix sessions
2022-07-07 15:49:23 +02:00
inverse_in_place
Initial bulk upgrade of z3
2023-04-13 09:43:18 +00:00
isqrt
separate transformations for intros, dequant, and remove_unused
2023-04-25 12:20:08 +00:00
isqrt_von_neumann
Initial bulk upgrade of z3
2023-04-13 09:43:18 +00:00
kleene_algebra
separate transformations for intros, dequant, and remove_unused
2023-04-25 12:20:08 +00:00
kmp
separate transformations for intros, dequant, and remove_unused
2023-04-25 12:20:08 +00:00
knuth_prime_numbers
update sessions, including prover upgrade Alt-Ergo 2.0.0 -> 2.1.0 when possible
2023-04-05 13:48:22 +02:00
koda_ruskey
separate transformations for intros, dequant, and remove_unused
2023-04-25 12:20:08 +00:00
largest_prime_factor
update sessions, including prover upgrade Alt-Ergo 2.0.0 -> 2.1.0 when possible
2023-04-05 13:48:22 +02:00
lcp
update sessions, including prover upgrade Alt-Ergo 2.0.0 -> 2.1.0 when possible
2023-04-05 13:48:22 +02:00
leftist_heap
separate transformations for intros, dequant, and remove_unused
2023-04-25 12:20:08 +00:00
linear_probing
separate transformations for intros, dequant, and remove_unused
2023-04-25 12:20:08 +00:00
linked_list_rev
separate transformations for intros, dequant, and remove_unused
2023-04-25 12:20:08 +00:00
list_removal
separate transformations for intros, dequant, and remove_unused
2023-04-25 12:20:08 +00:00
locate_max
Initial bulk upgrade of z3
2023-04-13 09:43:18 +00:00
logic
Initial bulk upgrade of z3
2023-04-13 09:43:18 +00:00
max_matrix
Initial bulk upgrade of z3
2023-04-13 09:43:18 +00:00
maximum_subarray
upgrade proofs with Z3 4.6.0 to 4.7.1
2023-04-07 09:37:36 +00:00
mccarthy
update sessions, including prover upgrade Alt-Ergo 2.0.0 -> 2.1.0 when possible
2023-04-05 13:48:22 +02:00
mccarthy_vc_sp
Initial bulk upgrade of z3
2023-04-13 09:43:18 +00:00
mergesort_array
Add "remove_unused:dependency" to int.ComputerDivision
2022-09-21 20:15:46 +00:00
mergesort_list
separate transformations for intros, dequant, and remove_unused
2023-04-25 12:20:08 +00:00
mergesort_queue
separate transformations for intros, dequant, and remove_unused
2023-04-25 12:20:08 +00:00
mex
separate transformations for intros, dequant, and remove_unused
2023-04-25 12:20:08 +00:00
micro-c
Add "remove_unused:dependency" to int.ComputerDivision
2022-09-21 20:15:46 +00:00
min_max
separate transformations for intros, dequant, and remove_unused
2023-04-25 12:20:08 +00:00
mjrty
Initial bulk upgrade of z3
2023-04-13 09:43:18 +00:00
mlcfg
need to eliminate_builtin before remove_unused
2023-03-06 22:20:36 +00:00
muller
fix sessions
2022-07-07 15:49:23 +02:00
multiprecision
separate transformations for intros, dequant, and remove_unused
2023-04-25 12:20:08 +00:00
mutual_recursion
separate transformations for intros, dequant, and remove_unused
2023-04-25 12:20:08 +00:00
my_cosine
update sessions, including prover upgrade Alt-Ergo 2.0.0 -> 2.1.0 when possible
2023-04-05 13:48:22 +02:00
nistonacci
fix sessions
2022-07-07 15:49:23 +02:00
optimal_replay
Initial bulk upgrade of z3
2023-04-13 09:43:18 +00:00
pairing_heap
separate transformations for intros, dequant, and remove_unused
2023-04-25 12:20:08 +00:00
pairing_heap_bin
separate transformations for intros, dequant, and remove_unused
2023-04-25 12:20:08 +00:00
pancake_sorting
Add "remove_unused:dependency" to int.ComputerDivision
2022-09-21 20:15:46 +00:00
patience
separate transformations for intros, dequant, and remove_unused
2023-04-25 12:20:08 +00:00
pigeonhole
update sessions, including prover upgrade Alt-Ergo 2.0.0 -> 2.1.0 when possible
2023-04-05 13:48:22 +02:00
power
separate transformations for intros, dequant, and remove_unused
2023-04-25 12:20:08 +00:00
power_vc_sp
separate transformations for intros, dequant, and remove_unused
2023-04-25 12:20:08 +00:00
prover
resurrect mark-obsolete and filters in why3 session update
2023-05-05 10:16:48 +02:00
python
separate transformations for intros, dequant, and remove_unused
2023-04-25 12:20:08 +00:00
queens
separate transformations for intros, dequant, and remove_unused
2023-04-25 12:20:08 +00:00
queens_bv
Initial bulk upgrade of z3
2023-04-13 09:43:18 +00:00
queue_two_lists
separate transformations for intros, dequant, and remove_unused
2023-04-25 12:20:08 +00:00
quicksort
fix sessions
2022-07-07 15:49:23 +02:00
random_access_list
separate transformations for intros, dequant, and remove_unused
2023-04-25 12:20:08 +00:00
register_allocation
update sessions, including prover upgrade Alt-Ergo 2.0.0 -> 2.1.0 when possible
2023-04-05 13:48:22 +02:00
relabel
update sessions, including prover upgrade Alt-Ergo 2.0.0 -> 2.1.0 when possible
2023-04-05 13:48:22 +02:00
remove_duplicate
update sessions, including prover upgrade Alt-Ergo 2.0.0 -> 2.1.0 when possible
2023-04-05 13:48:22 +02:00
remove_duplicate_hash
fix sessions
2022-07-07 15:49:23 +02:00
residual
separate transformations for intros, dequant, and remove_unused
2023-04-25 12:20:08 +00:00
resizable_array
update sessions, including prover upgrade Alt-Ergo 2.0.0 -> 2.1.0 when possible
2023-04-05 13:48:22 +02:00
rightmostbittrick
Initial bulk upgrade of z3
2023-04-13 09:43:18 +00:00
ring_buffer
fix sessions
2022-07-07 15:49:23 +02:00
ring_decision
Initial bulk upgrade of z3
2023-04-13 09:43:18 +00:00
ropes
Initial bulk upgrade of z3
2023-04-13 09:43:18 +00:00
same_fringe
update sessions, including prover upgrade Alt-Ergo 2.0.0 -> 2.1.0 when possible
2023-04-05 13:48:22 +02:00
schorr_waite
update sessions, including prover upgrade Alt-Ergo 2.0.0 -> 2.1.0 when possible
2023-04-05 13:48:22 +02:00
schorr_waite_via_recursion
update sessions, including prover upgrade Alt-Ergo 2.0.0 -> 2.1.0 when possible
2023-04-05 13:48:22 +02:00
schorr_waite_with_ghost_monitor
fix sessions
2022-07-07 15:49:23 +02:00
selection_sort
update sessions, including prover upgrade Alt-Ergo 2.0.0 -> 2.1.0 when possible
2023-04-05 13:48:22 +02:00
sf
fix session
2023-04-10 10:18:01 +02:00
sieve
Initial bulk upgrade of z3
2023-04-13 09:43:18 +00:00
skew_heaps
separate transformations for intros, dequant, and remove_unused
2023-04-25 12:20:08 +00:00
snapshotable_trees
update sessions, including prover upgrade Alt-Ergo 2.0.0 -> 2.1.0 when possible
2023-04-05 13:48:22 +02:00
sorted_list
update sessions, including prover upgrade Alt-Ergo 2.0.0 -> 2.1.0 when possible
2023-04-05 13:48:22 +02:00
space_saving
space-saving example: general case
2023-05-10 20:34:28 +02:00
stackify
Move stackify tests to stackify directory
2023-02-06 16:03:19 +01:00
stdlib
Merge attemp
2023-05-17 11:15:20 +02:00
string_base64_encoding
Initial bulk upgrade of z3
2023-04-13 09:43:18 +00:00
string_hex_encoding
Add "remove_unused:dependency" to int.ComputerDivision
2022-09-21 20:15:46 +00:00
string_search
separate transformations for intros, dequant, and remove_unused
2023-04-25 12:20:08 +00:00
subsequence
separate transformations for intros, dequant, and remove_unused
2023-04-25 12:20:08 +00:00
sudoku
Initial bulk upgrade of z3
2023-04-13 09:43:18 +00:00
sumrange
Initial bulk upgrade of z3
2023-04-13 09:43:18 +00:00
swap
update sessions, including prover upgrade Alt-Ergo 2.0.0 -> 2.1.0 when possible
2023-04-05 13:48:22 +02:00
tests
separate transformations for intros, dequant, and remove_unused
2023-04-25 12:20:08 +00:00
tests-provers
fix session
2023-04-30 11:19:27 +02:00
there_and_back_again
update sessions, including prover upgrade Alt-Ergo 2.0.0 -> 2.1.0 when possible
2023-04-05 13:48:22 +02:00
three_idem_ring
separate transformations for intros, dequant, and remove_unused
2023-04-25 12:20:08 +00:00
topological_sorting
update sessions, including prover upgrade Alt-Ergo 2.0.0 -> 2.1.0 when possible
2023-04-05 13:48:22 +02:00
tortoise_and_hare
separate transformations for intros, dequant, and remove_unused
2023-04-25 12:20:08 +00:00
tower_of_hanoi
update sessions, including prover upgrade Alt-Ergo 2.0.0 -> 2.1.0 when possible
2023-04-05 13:48:22 +02:00
toy_compiler
update sessions, including prover upgrade Alt-Ergo 2.0.0 -> 2.1.0 when possible
2023-04-05 13:48:22 +02:00
tree_height
separate transformations for intros, dequant, and remove_unused
2023-04-25 12:20:08 +00:00
tree_of_array
separate transformations for intros, dequant, and remove_unused
2023-04-25 12:20:08 +00:00
tree_of_list
separate transformations for intros, dequant, and remove_unused
2023-04-25 12:20:08 +00:00
unraveling_a_card_trick
update sessions, including prover upgrade Alt-Ergo 2.0.0 -> 2.1.0 when possible
2023-04-05 13:48:22 +02:00
use_api
Add a constructor for epsilon-terms in Ptree API
2023-05-15 09:52:03 +00:00
vacid_0_binary_heaps
Add "remove_unused:dependency" to int.ComputerDivision
2022-09-21 20:15:46 +00:00
vacid_0_build_maze
update sessions, including prover upgrade Alt-Ergo 2.0.0 -> 2.1.0 when possible
2023-04-05 13:48:22 +02:00
vacid_0_red_black_trees
separate transformations for intros, dequant, and remove_unused
2023-04-25 12:20:08 +00:00
vacid_0_sparse_array
update sessions, including prover upgrade Alt-Ergo 2.0.0 -> 2.1.0 when possible
2023-04-05 13:48:22 +02:00
verifythis_2015_dancing_links
update sessions, including prover upgrade Alt-Ergo 2.0.0 -> 2.1.0 when possible
2023-04-05 13:48:22 +02:00
verifythis_2015_parallel_gcd
separate transformations for intros, dequant, and remove_unused
2023-04-25 12:20:08 +00:00
verifythis_2015_relaxed_prefix
fix sessions
2022-07-07 15:49:23 +02:00
verifythis_2016_matrix_multiplication
separate transformations for intros, dequant, and remove_unused
2023-04-25 12:20:08 +00:00
verifythis_2016_tree_traversal
fix sessions
2022-07-07 15:49:23 +02:00
verifythis_2017_maximum_sum_submatrix
Initial bulk upgrade of z3
2023-04-13 09:43:18 +00:00
verifythis_2017_odd_even_sort_rearranging
upgrade proofs with Z3 4.6.0 to 4.7.1
2023-04-07 09:37:36 +00:00
verifythis_2017_odd_even_transposition_sort
Initial bulk upgrade of z3
2023-04-13 09:43:18 +00:00
verifythis_2017_pair_insertion_sort
Initial bulk upgrade of z3
2023-04-13 09:43:18 +00:00
verifythis_2017_tree_buffer
Initial bulk upgrade of z3
2023-04-13 09:43:18 +00:00
verifythis_2018_array_based_queuing_lock_1
Initial bulk upgrade of z3
2023-04-13 09:43:18 +00:00
verifythis_2018_array_based_queuing_lock_2
separate transformations for intros, dequant, and remove_unused
2023-04-25 12:20:08 +00:00
verifythis_2018_le_rouge_et_le_noir_1
separate transformations for intros, dequant, and remove_unused
2023-04-25 12:20:08 +00:00
verifythis_2018_le_rouge_et_le_noir_2
fix sessions
2022-07-07 14:15:53 +02:00
verifythis_2018_mind_the_gap_1
update sessions, including prover upgrade Alt-Ergo 2.0.0 -> 2.1.0 when possible
2023-04-05 13:48:22 +02:00
verifythis_2018_mind_the_gap_2
Initial bulk upgrade of z3
2023-04-13 09:43:18 +00:00
verifythis_2018_register_allocation
separate transformations for intros, dequant, and remove_unused
2023-04-25 12:20:08 +00:00
verifythis_2019_cartesian_trees
separate transformations for intros, dequant, and remove_unused
2023-04-25 12:20:08 +00:00
verifythis_2019_ghc_sort
separate transformations for intros, dequant, and remove_unused
2023-04-25 12:20:08 +00:00
verifythis_2021_dll_to_bst
separate transformations for intros, dequant, and remove_unused
2023-04-25 12:20:08 +00:00
verifythis_2021_lexicographic_permutations_1
separate transformations for intros, dequant, and remove_unused
2023-04-25 12:20:08 +00:00
verifythis_2021_lexicographic_permutations_2
separate transformations for intros, dequant, and remove_unused
2023-04-25 12:20:08 +00:00
verifythis_2021_shearsort
Add "remove_unused:dependency" to int.ComputerDivision
2022-09-21 20:15:46 +00:00
verifythis_2021_shearsort_modified
separate transformations for intros, dequant, and remove_unused
2023-04-25 12:20:08 +00:00
verifythis_fm2012_LRS
Initial bulk upgrade of z3
2023-04-13 09:43:18 +00:00
verifythis_fm2012_treedel
update sessions, including prover upgrade Alt-Ergo 2.0.0 -> 2.1.0 when possible
2023-04-05 13:48:22 +02:00
verifythis_PrefixSumRec
Fix sessions.
2023-01-31 01:50:53 +01:00
vstte10_aqueue
update sessions, including prover upgrade Alt-Ergo 2.0.0 -> 2.1.0 when possible
2023-04-05 13:48:22 +02:00
vstte10_inverting
Initial bulk upgrade of z3
2023-04-13 09:43:18 +00:00
vstte10_max_sum
update sessions, including prover upgrade Alt-Ergo 2.0.0 -> 2.1.0 when possible
2023-04-05 13:48:22 +02:00
vstte10_queens
Add "remove_unused:dependency" to int.ComputerDivision
2022-09-21 20:15:46 +00:00
vstte10_search_list
update sessions, including prover upgrade Alt-Ergo 2.0.0 -> 2.1.0 when possible
2023-04-05 13:48:22 +02:00
vstte12_bfs
fix sessions
2022-07-07 15:49:23 +02:00
vstte12_combinators
separate transformations for intros, dequant, and remove_unused
2023-04-25 12:20:08 +00:00
vstte12_ring_buffer
Initial bulk upgrade of z3
2023-04-13 09:43:18 +00:00
vstte12_tree_reconstruction
Initial bulk upgrade of z3
2023-04-13 09:43:18 +00:00
vstte12_two_way_sort
update sessions, including prover upgrade Alt-Ergo 2.0.0 -> 2.1.0 when possible
2023-04-05 13:48:22 +02:00
warshall_algorithm
Initial bulk upgrade of z3
2023-04-13 09:43:18 +00:00
white_and_black_balls
Add "remove_unused:dependency" to int.ComputerDivision
2022-09-21 20:15:46 +00:00
word_common_factor
separate transformations for intros, dequant, and remove_unused
2023-04-25 12:20:08 +00:00
WP_revisited
Initial bulk upgrade of z3
2023-04-13 09:43:18 +00:00
wrap_lines
separate transformations for intros, dequant, and remove_unused
2023-04-25 12:20:08 +00:00
zeros
update sessions, including prover upgrade Alt-Ergo 2.0.0 -> 2.1.0 when possible
2023-04-05 13:48:22 +02:00
add_list_vc_sp.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
add_list.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
algo63.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
algo64.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
algo65.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
all_distinct.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
amortization.mlw
a simple example of amortization
2021-04-01 13:47:23 +02:00
arm.mlw
Generalization of check_unused_vars to logic and program decl
2019-08-20 15:48:44 +02:00
array_most_frequent.mlw
examples: updated files for the gallery
2020-03-04 15:56:23 +01:00
assigning_meanings_to_programs.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
bag.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
balance.mlw
gallery: improve balance example even more
2023-04-07 10:59:08 +02:00
bellman_ford.mlw
no more libraries appmap and impmap
2020-02-11 17:56:34 +01:00
bench.sh
…
bignum.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
binary_multiplication.mlw
new example: binary_multiplication with 63-bit integers
2018-10-04 16:47:09 +02:00
binary_search_vc_sp.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
binary_search.mlw
improved binary_search.Complexity
2021-01-29 18:20:02 +01:00
binary_sort.mlw
Matrix: add the pure "update" function for applicative updates
2018-07-02 17:15:42 +02:00
binary_sqrt.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
binomial_heap.mlw
No more let empty () = ... in examples.
2020-09-10 18:13:14 +01:00
binomial.mlw
new example: binomial coefficient
2023-02-17 19:31:10 +01:00
bitcount.mlw
Several renamings and fix a few pre and post-conditions
2021-09-29 08:57:02 +02:00
bitvector_examples.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
bitwalker.mlw
Several renamings and fix a few pre and post-conditions
2021-09-29 08:57:02 +02:00
braun_trees.mlw
gallery: two return types added
2022-12-01 20:02:29 +01:00
bresenham.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
bubble_sort.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
checking_a_large_routine.mlw
examples: variant of Turing's factorial
2022-08-26 11:27:04 +02:00
coincidence_count_list.mlw
stdlib: set library revamped
2019-03-07 11:13:49 +01:00
coincidence_count.mlw
coincidence_count example: added a bag version
2020-12-05 11:02:11 +01:00
conjugate.mlw
conjugate: a 32-bit implementation, which extracts to C
2019-07-04 16:39:58 +02:00
counting_sort.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
cubic_root.mlw
example cubic_root: nicer code using auto deref
2020-03-04 16:11:49 +01:00
cursor_examples.mlw
examples: document cursor_examples
2020-03-04 16:57:26 +01:00
decrease1.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
defunctionalization.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
dfa_example.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
dfs.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
dijkstra.mlw
no more libraries appmap and impmap
2020-02-11 17:56:34 +01:00
disamb.mlw
more comments on the disamb example
2020-10-01 15:50:36 +02:00
division.mlw
new example: Hoare's Euclidean division
2021-03-08 12:39:31 +01:00
dyck.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
edit_distance.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
equality_up_to_spaces.mlw
Fix examples so they don't define type string
2019-09-23 11:14:46 +02:00
esterel.mlw
stdlib: set library revamped
2019-03-07 11:13:49 +01:00
euler001.mlw
Update comment.
2022-10-25 05:24:17 +02:00
euler002.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
euler011.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
euler_sieve.mlw
fix sessions
2021-06-25 14:15:38 +02:00
ewd673.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
f_puzzle.mlw
Change extension to mlw.
2020-03-05 09:17:48 +01:00
fact_vc_sp.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
fact.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
fenwick.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
fib_memo.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
fibonacci.mlw
fix sessions
2022-07-30 11:40:25 +02:00
fill.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
find.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
finger_trees.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
finite_tarski.mlw
stdlib: set library revamped
2019-03-07 11:13:49 +01:00
flag2.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
flag.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
flexible_arrays.mlw
flexible arrays: more operations
2023-04-18 14:35:23 +02:00
foveoos11_challenge1.mlw
gallery: foveoos11_challenge1 using auto-deref
2019-02-18 14:08:58 +01:00
foveoos11_challenge2.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
foveoos11_challenge3.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
gcd_bezout_vc_sp.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
gcd_bezout.mlw
gcd_bezout: slightly nicer code
2018-09-05 16:53:27 +02:00
gcd_vc_sp.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
gcd.mlw
more autodereference in the gallery
2020-06-25 10:49:12 +02:00
generate_all_trees.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
gnome_sort.mlw
gnome sort with auto-dereference
2021-01-28 09:17:00 +01:00
hackers-delight.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
hashtbl_impl.mlw
Ity: in cty, remove writes which are invalidated by resets
2019-01-18 18:26:34 +01:00
hello-world.mlw
Printer for string literals with escape sequences.
2019-10-22 16:26:19 +02:00
hillel_challenge.mlw
stdlib: new library fmap
2019-11-08 16:59:54 +01:00
huffman_with_two_queues.mlw
library: new theory seq.Sum
2019-05-08 22:30:01 +02:00
i_cant_believe_it_can_sort.mlw
cleaning up
2022-07-04 11:28:47 +02:00
incremental.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
induction.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
infinity_of_primes.mlw
new example: infinity_of_primes
2021-06-11 14:37:03 +02:00
insertion_sort_list.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
insertion_sort_naive.mlw
insertion_sort: cleaning up, auto deref, swap version
2021-03-18 18:33:45 +01:00
insertion_sort.mlw
insertion_sort: cleaning up, auto deref, swap version
2021-03-18 18:33:45 +01:00
inverse_in_place.mlw
inverse_in_place with auto-dereference
2019-07-04 10:39:55 +02:00
isqrt_von_neumann.mlw
example isqrt von neumann: improve comments
2020-03-04 16:21:29 +01:00
isqrt.mlw
add default names for program annotations
2019-06-07 15:06:30 +02:00
kleene_algebra.mlw
kleene_algebra example: no more unnecessary axioms
2021-06-27 18:56:11 +02:00
kmp.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
knuth_prime_numbers.mlw
knuth_prime_numbers: two minor, cosmetic changes
2018-11-20 09:53:04 +01:00
koda_ruskey.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
largest_prime_factor.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
lcp.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
leftist_heap.mlw
No more let empty () = ... in examples.
2020-09-10 18:13:14 +01:00
linear_probing.mlw
Ity: in cty, remove writes which are invalidated by resets
2019-01-18 18:26:34 +01:00
linked_list_rev.mlw
gallery: list reversal terminates, even on cyclic lists
2022-11-06 00:02:54 +01:00
list_removal.mlw
one writes in enough
2021-03-16 14:55:20 +01:00
locate_max.mlw
Document the extraction to C.
2022-05-11 17:46:27 +02:00
max_matrix.mlw
no more theory sum.Sum
2020-02-12 10:30:25 +01:00
maximum_subarray.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
mccarthy_vc_sp.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
mccarthy.mlw
gallery: yet another implementation of McCarthy's 91 function
2018-12-11 23:03:55 +01:00
mergesort_array.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
mergesort_list.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
mergesort_queue.mlw
updated proof sessions
2019-06-05 17:55:47 +02:00
mex.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
min_max.mlw
min_max: a divide and conquer solution
2020-02-14 09:06:31 +01:00
mjrty.mlw
new example: space saving algorithm
2023-05-09 15:54:05 +02:00
muller.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
mutual_recursion.mlw
modified example mutual_recursion
2020-05-01 21:05:40 +02:00
my_cosine.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
nistonacci.mlw
New very simple example: Nistonacci numbers
2018-06-28 17:27:29 +02:00
optimal_replay.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
pairing_heap_bin.mlw
No more let empty () = ... in examples.
2020-09-10 18:13:14 +01:00
pairing_heap.mlw
No more let empty () = ... in examples.
2020-09-10 18:13:14 +01:00
pancake_sorting.mlw
new example: pancake sorting
2018-08-24 11:26:16 +02:00
patience.mlw
Generalization of check_unused_vars to logic and program decl
2019-08-20 15:48:44 +02:00
pigeonhole.mlw
stdlib: set library revamped
2019-03-07 11:13:49 +01:00
power_vc_sp.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
power.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
queens_bv.mlw
stdlib: set library revamped
2019-03-07 11:13:49 +01:00
queens.mlw
No more let empty () = ... in examples.
2020-09-10 18:13:14 +01:00
queue_two_lists.mlw
Merge remote-tracking branch 'origin/master' into fixclone
2020-03-16 20:52:59 +01:00
quicksort.mlw
examples: yet another version of quicksort
2021-01-13 11:10:32 +01:00
random_access_list.mlw
No more let empty () = ... in examples.
2020-09-10 18:13:14 +01:00
reduced_regtests.list
Remove rightmostbittrick from CI, as it fails a bit too often.
2019-11-15 14:45:54 +01:00
register_allocation.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
regtests.out
Fix sessions and update oracles for result variables in VC SP
2021-10-04 15:53:08 +02:00
regtests.sh
Add flags to toggle every warning
2023-04-03 17:14:10 +02:00
relabel.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
remove_duplicate_hash.mlw
stdlib: set library revamped
2019-03-07 11:13:49 +01:00
remove_duplicate.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
residual.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
resizable_array.mlw
Dexpr: emit a warning for spurious olds in val contracts
2021-03-12 20:56:41 +01:00
rightmostbittrick.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
ring_buffer.mlw
examples: simple_queue -> ring_buffer
2020-03-04 15:56:23 +01:00
ropes.mlw
No more let empty () = ... in examples.
2020-09-10 18:13:14 +01:00
same_fringe.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
schorr_waite_via_recursion.mlw
stdlib: set library revamped
2019-03-07 11:13:49 +01:00
schorr_waite_with_ghost_monitor.mlw
stdlib: set library revamped
2019-03-07 11:13:49 +01:00
schorr_waite.mlw
stdlib: set library revamped
2019-03-07 11:13:49 +01:00
selection_sort.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
sf.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
sieve.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
skew_heaps.mlw
No more let empty () = ... in examples.
2020-09-10 18:13:14 +01:00
snapshotable_trees.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
sorted_list.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
space_saving.mlw
space-saving example: general case
2023-05-10 20:34:28 +02:00
string_base64_encoding.mlw
minor cosmetic fix base64 example
2020-07-28 15:05:45 +02:00
string_hex_encoding.mlw
Documentation for Hexadecimal encoding
2020-03-04 15:31:05 +01:00
string_search.mlw
a better way to provide that the length of string is nonnegative
2020-06-19 14:04:36 +02:00
subsequence.mlw
new example: subsequences
2019-05-19 14:13:06 +02:00
sudoku.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
sumrange.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
swap.mlw
example: swapping two integers
2020-04-29 13:12:53 +02:00
there_and_back_again.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
three_idem_ring.mlw
Unified format for new examples
2019-11-06 15:47:00 +01:00
TODO
…
topological_sorting.mlw
no more libraries appmap and impmap
2020-02-11 17:56:34 +01:00
tortoise_and_hare.mlw
fix sessions
2021-06-25 15:01:56 +02:00
tower_of_hanoi.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
toy_compiler.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
tree_height.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
tree_of_array.mlw
fix some broken proofs
2018-09-05 11:31:25 +02:00
tree_of_list.mlw
fix broken proof
2018-09-05 13:04:00 +02:00
unraveling_a_card_trick.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
vacid_0_build_maze.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
vacid_0_red_black_trees.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
vacid_0_sparse_array.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
verifythis_2015_dancing_links.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
verifythis_2015_parallel_gcd.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
verifythis_2015_relaxed_prefix.mlw
Fix invalid html.
2018-06-24 10:37:12 +02:00
verifythis_2016_tree_traversal.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
verifythis_2017_maximum_sum_submatrix.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
verifythis_2017_odd_even_sort_rearranging.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
verifythis_2017_odd_even_transposition_sort.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
verifythis_2017_pair_insertion_sort.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
verifythis_2017_tree_buffer.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
verifythis_2018_array_based_queuing_lock_1.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
verifythis_2018_array_based_queuing_lock_2.mlw
Update ABQL session
2019-06-06 16:39:35 +02:00
verifythis_2018_le_rouge_et_le_noir_1.mlw
Generalization of check_unused_vars to logic and program decl
2019-08-20 15:48:44 +02:00
verifythis_2018_le_rouge_et_le_noir_2.mlw
examples/ fix name-shadowing conflicts due to the new Array.empty
2019-06-24 18:12:57 +02:00
verifythis_2018_mind_the_gap_1.mlw
Generalization of check_unused_vars to logic and program decl
2019-08-20 15:48:44 +02:00
verifythis_2018_mind_the_gap_2.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
verifythis_2018_register_allocation.mlw
simplifies fib tail rec proof and add counterexample to regalloc as a comment
2021-09-16 16:33:30 +02:00
verifythis_2019_cartesian_trees.mlw
Unified format for new examples
2019-11-06 15:47:00 +01:00
verifythis_2019_ghc_sort.mlw
Unified format for new examples
2019-11-06 15:47:00 +01:00
verifythis_2021_dll_to_bst.mlw
typo
2023-02-17 13:32:33 +01:00
verifythis_2021_lexicographic_permutations_1.mlw
Add another way to complete challenge 1 from VerifyThis 2021
2021-04-26 13:59:20 +00:00
verifythis_2021_lexicographic_permutations_2.mlw
Add another way to complete challenge 1 from VerifyThis 2021
2021-04-26 13:59:20 +00:00
verifythis_2021_shearsort_modified.mlw
fix euler_sieve, array and split_vc interaction
2021-04-30 10:48:03 +02:00
verifythis_2021_shearsort.mlw
Add another way to complete challenge 1 from VerifyThis 2021
2021-04-26 13:59:20 +00:00
verifythis_fm2012_LRS.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
verifythis_fm2012_treedel.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
verifythis_PrefixSumRec.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
vstte10_aqueue.mlw
No more let empty () = ... in examples.
2020-09-10 18:13:14 +01:00
vstte10_inverting.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
vstte10_max_sum.mlw
simplified proof sessions
2020-02-14 12:08:42 +01:00
vstte10_queens.mlw
Generalization of check_unused_vars to logic and program decl
2019-08-20 15:48:44 +02:00
vstte10_search_list.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
vstte12_bfs.mlw
stdlib: set library revamped
2019-03-07 11:13:49 +01:00
vstte12_combinators.mlw
support for algebraic types simplify some proofs.
2023-01-31 08:25:07 +01:00
vstte12_ring_buffer.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
vstte12_tree_reconstruction.mlw
vstte12_tree_reconstruction: fix Coq proof
2019-08-21 12:55:22 +02:00
vstte12_two_way_sort.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
warshall_algorithm.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00
white_and_black_balls.mlw
example white_and_black_balls: nicer code using auto deref
2020-03-04 16:48:11 +01:00
word_common_factor.mlw
word_common_factor: simplified proof
2019-04-02 17:30:14 +02:00
wrap_lines.mlw
examples/wrap_lines: extended challenge
2021-03-27 19:48:42 +01:00
zeros.mlw
stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00