Skip to content

Instantly share code, notes, and snippets.

@gnn

gnn/sorting.dol

Last active August 18, 2016 17:03
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save gnn/10be7711f53d9bca2d4416d2ba54fc32 to your computer and use it in GitHub Desktop.
Save gnn/10be7711f53d9bca2d4416d2ba54fc32 to your computer and use it in GitHub Desktop.
Download ZIP
A proposed fix for the "attempt to hide ... from the local environment" error
Raw
sorting.dol
spec Sorting =
TotalOrder and List
then {
preds is_ordered : List;
permutation : List * List
vars x,y:Elem; L,L1,L2:List
. is_ordered([])
. is_ordered(x::[])
. is_ordered(x::y::L) <=> x<=y /\ is_ordered(y::L)
. permutation(L1,L2) <=> (forall x:Elem . count(x,L1) = count(x,L2))
then
op sorter : List->List
var L:List
. is_ordered(sorter(L))
. permutation(L,sorter(L))
} hide is_ordered, permutation
end
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment