Pierre Letouzey edited this page Oct 27, 2017 · 4 revisions

Notation for List Comprehension

We want to define a notation for Haskell-like list comprehension using Notation, ie we want to denote

[ b | b <- l , P(b) ]

in Coq.

Assuming we have a variable list_comprehension that has the following type:

Variable list_comprehension: forall A : Set, list A -> forall P : A -> Prop, is_decidable A P -> list A.
Implicit Arguments list_comprehension [A].


Definition is_decidable (A:Set) (P:A->Prop) := forall a, {P a} + {~(P a)}.

we can declare the following notation.

Notation "[ e | b <- l , Hp ]" := (map (fun b:_=> e) (list_comprehension l (fun b:_=>_ ) Hp))  (at level 1).

Now, for example, if

Hypothesis  Zlt_decide:forall a, is_decidable Z (fun x=>x<a).

we can use the above notation to define the Haskell list [ y | y<-l , y<pivot] where l:list Z and pivot:Z:

Definition elt_lt_x l pivot:= [ y | y <- l , (Zlt_decide pivot) ].
Clone this wiki locally
You can’t perform that action at this time.
You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session.
Press h to open a hovercard with more details.