Skip to content

Instantly share code, notes, and snippets.

@mbrcknl

mbrcknl/SortingFunction.v

Created December 9, 2015 21:53
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 mbrcknl/0141aa8a9cff9482743a to your computer and use it in GitHub Desktop.
Save mbrcknl/0141aa8a9cff9482743a to your computer and use it in GitHub Desktop.
Download ZIP
Raw
SortingFunction.v
Require Import Sorted.
Require Import Permutation.
Definition isSortingFunction (A: Type) (R: A -> A -> Prop) (f: list A -> list A): Prop :=
forall (xs: list A), Permutation xs (f xs) /\ Sorted R (f xs).
Check (isSortingFunction: forall (A: Type), (A -> A -> Prop) -> (list A -> list A) -> Prop).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment