---------- Forwarded message ---------
From: Shenghao <shy...@nuaa.edu.cn>
Date: Tue, Aug 11, 2020 at 9:44 AM
Subject: Quicksort in the tutorial
To: <fstar-club-ow...@lists.gforge.inria.fr>
Hello,
I'm doing exercises in the tutorial ( a F* newbie).
In section 6.1.2 Specifying sort,
val sort_tweaked: l:list int -> Tot (m:list int{sorted m /\ (forall i.
mem i l = mem i m)})
(decreases (length l))let rec
sort_tweaked l = match l with
| [] -> []
| pivot :: tl ->
let hi', lo' = partition (cmp pivot) tl in
partition_lemma (cmp pivot) tl;
let hi = sort_tweaked hi' in
let lo = sort_tweaked lo' in
append_mem lo (pivot :: hi);
sorted_concat_lemma lo hi pivot;
append lo (pivot :: hi)
I find it fails to compile when I replace the refinement type
"m:list int{sorted m /\ (forall i. mem i l = mem i m)}" with "m:list int{
sorted m}", just deleting the latter property. The terminal reports:
"(Error 19) assertion failed"
How can I compile the new version successfully? Could you please
give me some suggestions? Thanks a lot!
Best wishes,
--
Shenghao Yuan
College of Computer Science and Technology (CCST)
Nanjing University of Aeronautics and Astronautics (NUAA)
Nanjing China
_______________________________________________
fstar-club mailing list
fstar-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/fstar-club
